From Coq Require Import FunctionalExtensionality.
Tutorial: VLSMs that Multiply
#[local] Open Scope Z_scope.
Definition of common features of the multiplying VLSMs
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) 1done. Defined. #[export] Instance multiplying_initial_state_type_inhabited : Inhabited (multiplying_initial_state_type) := populate (multiplying_initial_state).(λ st : multiplying_state, multiplying_initial_state_prop st) 1
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
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;
|}.
X: VLSM multiplying_messagetransition multiply_label (4, Some 10) = (-6, Some 20)done. Qed.X: VLSM multiplying_messagetransition multiply_label (4, Some 10) = (-6, Some 20)
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 2by apply initial_message_is_valid. Qed.valid_message_prop doubling_vlsm 2can_emit doubling_vlsm 4can_emit doubling_vlsm 4input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)valid_state_prop doubling_vlsm 2option_valid_message_prop doubling_vlsm (Some 2)by apply initial_state_is_valid; cbn; unfold multiplying_initial_state_prop; lia.valid_state_prop doubling_vlsm 2by app_valid_tran. Qed.option_valid_message_prop doubling_vlsm (Some 2)valid_message_prop doubling_vlsm 4by apply (emitted_messages_are_valid doubling_vlsm 4 doubling_can_emit_4). Qed.valid_message_prop doubling_vlsm 4input_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 8option_valid_message_prop doubling_vlsm (Some 4)2 ≤ 4by apply initial_state_is_valid; cbn; unfold multiplying_initial_state_prop, doubling_trace1_first_state; lia.valid_state_prop doubling_vlsm 8by apply doubling_valid_message_prop_4.option_valid_message_prop doubling_vlsm (Some 4)by unfold doubling_trace1_first_state; nia. Qed.2 ≤ 4input_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 4option_valid_message_prop doubling_vlsm (Some 2)by app_valid_tran; eapply doubling_valid_transition_1; lia.valid_state_prop doubling_vlsm 4by apply doubling_valid_message_prop_2. Qed.option_valid_message_prop doubling_vlsm (Some 2)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 2option_valid_message_prop doubling_vlsm (Some 2)by app_valid_tran; apply doubling_valid_transition_2.valid_state_prop doubling_vlsm 2by apply doubling_valid_message_prop_2. Qed.option_valid_message_prop doubling_vlsm (Some 2)finite_valid_trace_init_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1finite_valid_trace_init_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1finite_valid_trace_from_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1finite_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)by eapply finite_valid_trace_from_to_empty, input_valid_transition_destination, doubling_valid_transition_3.finite_valid_trace_from_to doubling_vlsm 0 doubling_trace1_last_state []by apply doubling_valid_transition_3.input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)by apply doubling_valid_transition_2.input_valid_transition doubling_vlsm multiply_label (4, Some 2) (2, Some 4)by apply doubling_valid_transition_1. Qed.input_valid_transition doubling_vlsm multiply_label (doubling_trace1_first_state, Some 4) (4, Some 8)finite_valid_trace_init_to_alt doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1finite_valid_trace_init_to_alt doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1by repeat apply mvt_extend; [.. | apply mvt_empty]; try done; [apply doubling_valid_message_prop_4 | apply doubling_valid_message_prop_2 ..]. Qed.message_valid_transitions_from_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1
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_trace1finite_constrained_trace_init_to_direct doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1by 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.constrained_transitions_from_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1
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)by app_valid_tran. Qed.input_valid_transition doubling_vlsm multiply_label (doubling_trace2_init_first_state, Some 2) (5, 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.input_valid_transition doubling_vlsm multiply_label (5, Some 2) (3, Some 4)finite_valid_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_initfinite_valid_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_initfinite_valid_trace_from_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_initfinite_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)by eapply finite_valid_trace_from_to_empty, input_valid_transition_destination, doubling_valid_transition_2'.finite_valid_trace_from_to doubling_vlsm 3 doubling_trace2_init_last_state []by apply doubling_valid_transition_2'.input_valid_transition doubling_vlsm multiply_label (5, Some 2) (3, Some 4)by apply doubling_valid_transition_1'. Qed.input_valid_transition doubling_vlsm multiply_label (doubling_trace2_init_first_state, Some 2) (5, Some 4)finite_valid_trace_init_to_alt doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_initfinite_valid_trace_init_to_alt doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_initby repeat apply mvt_extend; [..| apply mvt_empty]; try done; apply doubling_valid_message_prop_2. Qed.message_valid_transitions_from_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_init
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_initfinite_constrained_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_init_last_state doubling_trace2_initVLSM_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_initby apply vlsm_incl_preloaded.VLSM_incl_part doubling_machine (preloaded_vlsm_machine doubling_vlsm (λ _ : multiplying_message, True))by apply doubling_valid_trace2_init. Qed.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
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_trace2finite_constrained_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_last_state doubling_trace2H: 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_statefinite_constrained_trace_init_to doubling_vlsm doubling_trace2_init_first_state doubling_trace2_last_state doubling_trace2H: 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_statefinite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_last_state doubling_trace2H: 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_stateinput_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_statevalid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_last_stateH: 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_stateoption_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some 3)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_statevalid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_last_stateby apply any_message_is_valid_in_preloaded. Qed.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_stateoption_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some 3)
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)by apply doubling_valid_trace1. Qed.finite_valid_trace_from_to doubling_vlsm doubling_trace1_first_state doubling_trace1_last_state doubling_trace1
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)by apply doubling_constrained_trace2. Qed.finite_valid_trace_from_to (preloaded_with_all_messages_vlsm doubling_vlsm) doubling_trace2_init_first_state doubling_trace2_last_state doubling_trace2
VLSM_incl doubling_vlsm (preloaded_with_all_messages_vlsm doubling_vlsm)by apply vlsm_incl_preloaded_with_all_messages_vlsm. Qed.VLSM_incl doubling_vlsm (preloaded_with_all_messages_vlsm doubling_vlsm)
∀ 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 >= 4m: 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 >= 4by split; [eexists | lia]. Qed.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∀ 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 mn: Z
Hmgt0: 2 * n >= 4constrained_message_prop doubling_vlsm (2 * n)n: Z
Hmgt0: 2 * n >= 4input_valid_transition (preloaded_with_all_messages_vlsm doubling_vlsm) multiply_label (n, Some n) (0, Some (2 * n))n: Z
Hmgt0: 2 * n >= 4valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) nn: Z
Hmgt0: 2 * n >= 4option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some n)apply initial_state_is_valid; cbn; red; lia.n: Z
Hmgt0: 2 * n >= 4valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) nby apply any_message_is_valid_in_preloaded. Qed.n: Z
Hmgt0: 2 * n >= 4option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some n)∀ 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 >= 4m: multiplying_messageconstrained_message_prop doubling_vlsm m → Z.Even m ∧ m >= 4m: multiplying_messageZ.Even m ∧ m >= 4 → constrained_message_prop doubling_vlsm mby apply doubling_constrained_messages_left.m: multiplying_messageconstrained_message_prop doubling_vlsm m → Z.Even m ∧ m >= 4by intros [? ?]; apply doubling_constrained_messages_right. Qed.m: multiplying_messageZ.Even m ∧ m >= 4 → constrained_message_prop doubling_vlsm m
∀ st : multiplying_state, constrained_state_prop doubling_vlsm st → st >= 0∀ st : multiplying_state, constrained_state_prop doubling_vlsm st → st >= 0s: state (preloaded_with_all_messages_vlsm doubling_vlsm)
Hs: initial_state_prop ss >= 0s': 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 >= 0s' >= 0cbn in Hs; red in Hs; lia.s: state (preloaded_with_all_messages_vlsm doubling_vlsm)
Hs: initial_state_prop ss >= 0s': 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 >= 0s' >= 0by inversion Ht; subst; cbn in *; lia. Qed.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 >= 0s' >= 0∀ st : multiplying_state, st >= 0 → constrained_state_prop doubling_vlsm st∀ st : multiplying_state, st >= 0 → constrained_state_prop doubling_vlsm stst: multiplying_state
Hst: st >= 0constrained_state_prop doubling_vlsm stst: multiplying_state
Hst: st >= 0input_valid_transition (preloaded_with_all_messages_vlsm doubling_vlsm) multiply_label (st + 2, Some 2) (st, Some 4)st: multiplying_state
Hst: st >= 0valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (st + 2)st: multiplying_state
Hst: st >= 0option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some 2)apply initial_state_is_valid; cbn; red; lia.st: multiplying_state
Hst: st >= 0valid_state_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (st + 2)by apply any_message_is_valid_in_preloaded. Qed.st: multiplying_state
Hst: st >= 0option_valid_message_prop (preloaded_with_all_messages_vlsm doubling_vlsm) (Some 2)∀ st : multiplying_state, constrained_state_prop doubling_vlsm st ↔ st >= 0∀ st : multiplying_state, constrained_state_prop doubling_vlsm st ↔ st >= 0st: multiplying_stateconstrained_state_prop doubling_vlsm st → st >= 0st: multiplying_statest >= 0 → constrained_state_prop doubling_vlsm stby apply doubling_constrained_states_right.st: multiplying_stateconstrained_state_prop doubling_vlsm st → st >= 0by apply doubling_constrained_states_left. Qed.st: multiplying_statest >= 0 → constrained_state_prop doubling_vlsm st
∀ 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 ^ pm: multiplying_message
s: state doubling_vlsm
Hvsm: valid_state_message_prop doubling_vlsm s (Some m)∃ p : Z, p >= 1 ∧ m = 2 ^ pm: 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 ^ pm: 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 ^ pm: 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 ^ ps: 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 ^ ps: 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 ^ ps: 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 ^ pby exists 1; split; lia.s: multiplying_state
Hs: multiplying_initial_state_prop s∃ p : Z, p >= 1 ∧ 2 = 2 ^ ps: 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 ^ ps: 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 ^ ps: 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 ^ ps: 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 ^ ps: 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 >= 1 ∧ 2 * 2 ^ x = 2 ^ ps: 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 >= 1x + 1 >= 1 ∧ 2 * 2 ^ x = 2 ^ (x + 1)by rewrite <- Z.pow_succ_r; [| lia]. Qed.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 >= 12 * 2 ^ x = 2 ^ (x + 1)∀ 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 >= 1valid_message_prop doubling_vlsm (2 ^ p)p: Z
Hp: p >= 1
Hle: 0 ≤ p - 1valid_message_prop doubling_vlsm (2 ^ p)p: Z
Hp: p >= 1
Hle: 0 ≤ p - 1valid_message_prop doubling_vlsm (2 ^ (p - 1 + 1))p: Z
Hp: p >= 1
x: Z
Heqx: x = p - 1
Hle: 0 ≤ xvalid_message_prop doubling_vlsm (2 ^ (x + 1))x: Z
Hle: 0 ≤ xvalid_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))2 ≤ 2 ^ (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)))by apply initial_state_is_valid; cbn; red; lia.x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))valid_state_prop doubling_vlsm (2 ^ (x + 1))by apply Hindh.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))2 ≤ 2 ^ (x + 1)by rewrite Z.pow_succ_r; lia.x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))2 ≤ 2 ^ Z.succ xby lia.x: Z
Hxgt0: 0 ≤ x
Hindh: valid_message_prop doubling_vlsm (2 ^ (x + 1))2 ^ (x + 1) ≤ 2 ^ (x + 1)by cbn; rewrite <- Z.pow_succ_r, Z.add_succ_l; [do 2 f_equal; lia | lia]. Qed.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)))∀ 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_messagevalid_message_prop doubling_vlsm m → ∃ p : Z, p >= 1 ∧ m = 2 ^ pm: multiplying_message(∃ p : Z, p >= 1 ∧ m = 2 ^ p) → valid_message_prop doubling_vlsm mby intros; apply doubling_valid_messages_powers_of_2_right.m: multiplying_messagevalid_message_prop doubling_vlsm m → ∃ p : Z, p >= 1 ∧ m = 2 ^ pby intros (p & Hpgt0 & [= ->]); apply doubling_valid_messages_powers_of_2_left. Qed.m: multiplying_message(∃ p : Z, p >= 1 ∧ m = 2 ^ p) → valid_message_prop doubling_vlsm m
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)Falsep: Z
Hp: p >= 1
Heq: 3 = 2 ^ pFalseby rewrite Z.pow_succ_r in Heq; lia. Qed.p: Z
Hp: p >= 1
Heq: 3 = 2 ^ Z.succ (Z.pred p)False
s: multiplying_statevalid_state_prop doubling_vlsm s → s >= 0s: multiplying_statevalid_state_prop doubling_vlsm s → s >= 0s': 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 >= 0s' >= 0s': 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 >= 0s' >= 0by destruct Hv; lia. Qed.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 >= 0s - m >= 0s: multiplying_states >= 0 → valid_state_prop doubling_vlsm ss: multiplying_states >= 0 → valid_state_prop doubling_vlsm ss: multiplying_state
H: s >= 0valid_state_prop doubling_vlsm sH: 0 >= 0valid_state_prop doubling_vlsm 0H: 0 >= 0input_valid_transition doubling_vlsm multiply_label (2, Some 2) (0, Some 4)H: 0 >= 0valid_state_prop doubling_vlsm 2H: 0 >= 0option_valid_message_prop doubling_vlsm (Some 2)by apply initial_state_is_valid; cbn; red; lia.H: 0 >= 0valid_state_prop doubling_vlsm 2by apply initial_message_is_valid. Qed.H: 0 >= 0option_valid_message_prop doubling_vlsm (Some 2)∀ s : multiplying_state, valid_state_prop doubling_vlsm s ↔ s >= 0∀ s : multiplying_state, valid_state_prop doubling_vlsm s ↔ s >= 0s: multiplying_statevalid_state_prop doubling_vlsm s → s >= 0s: multiplying_states >= 0 → valid_state_prop doubling_vlsm sby apply doubling_valid_states_right.s: multiplying_statevalid_state_prop doubling_vlsm s → s >= 0by apply doubling_valid_states_left. Qed.s: multiplying_states >= 0 → valid_state_prop doubling_vlsm s
Definition of the tripling VLSM
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.
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 index23by 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.EqDecision index23
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 2by exists two; unshelve eexists (exist _ 2 _); cbn; lia. Qed.composite_initial_message_prop components_23 2composite_initial_message_prop components_23 3by exists three; unshelve eexists (exist _ 3 _); cbn; lia. Qed.composite_initial_message_prop components_23 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 ^ p3m: 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 ^ p3m: 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 ^ p3m: 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 ^ p3m: 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 ^ p3s: 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 ^ p3s: 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 ^ p3s: 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 ^ p3s: 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 ^ p3s: 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 ^ p3s: 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 ^ p3by exists 1, 0; split; lia.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 ^ p3by exists 0, 1; 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 ^ p3s: 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 ^ p3s: 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 >= 1 ∧ 2 * m = 2 ^ p2 * 3 ^ p3s: 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 >= 1 ∧ 3 * m = 2 ^ p2 * 3 ^ p3s: 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 >= 1 ∧ 2 * m = 2 ^ p2 * 3 ^ p3s: 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 ^ p3Z.succ p2 >= 0 ∧ p3 >= 0 ∧ Z.succ p2 + p3 >= 1 ∧ 2 * m = 2 ^ Z.succ p2 * 3 ^ p3by 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 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 ^ p3p3 >= 0 ∧ Z.succ p2 + p3 >= 1 ∧ 2 * m = 2 ^ Z.succ p2 * 3 ^ p3s: 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 >= 1 ∧ 3 * m = 2 ^ p2 * 3 ^ p3s: 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 ^ p3p2 >= 0 ∧ Z.succ p3 >= 0 ∧ p2 + Z.succ p3 >= 1 ∧ 3 * m = 2 ^ p2 * 3 ^ Z.succ p3by rewrite Z.pow_succ_r; lia. Qed.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 ^ p3Z.succ p3 >= 0 ∧ p2 + Z.succ p3 >= 1 ∧ 3 * m = 2 ^ p2 * 3 ^ Z.succ p3∀ p2 p3 : Z, p2 >= 0 → p3 >= 0 → 1 ≤ p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)∀ p2 p3 : Z, p2 >= 0 → p3 >= 0 → 1 ≤ p2 + p3 → valid_message_prop free_composition_23 (2 ^ p2 * 3 ^ p3)p2, p3: Z
Hp2: p2 >= 0
Hp3: p3 >= 0
Hp: 1 ≤ p2 + p3valid_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 ≤ pvalid_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 → PropP 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 >= 0valid_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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0valid_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 ≠ 0valid_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 ≠ 0valid_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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0valid_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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1valid_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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1can_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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1input_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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1valid_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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1option_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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 12 ≤ 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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 13 ^ (p3 - 1) ≤ state_23 1 (3 ^ (p3 - 1)) threep3: 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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1transition (existT three multiply_label) (state_23 1 (3 ^ (p3 - 1)), Some (3 ^ (p3 - 1))) = (state10, Some (2 ^ 0 * 3 ^ p3))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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1valid_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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1option_valid_message_prop free_composition_23 (Some (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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1option_valid_message_prop free_composition_23 (Some (2 ^ 0 * 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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 12 ≤ 3 ^ (p3 - 1)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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 12 ≤ 3 ^ Z.succ (p3 - 2)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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 13 ^ (p3 - 1) ≤ state_23 1 (3 ^ (p3 - 1)) threep3: 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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1transition (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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1state_update components_23 (state_23 1 (3 ^ (p3 - 1))) three (3 ^ (p3 - 1) - 3 ^ (p3 - 1)) = state10p3: 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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1Some (3 * 3 ^ (p3 - 1)) = Some (2 ^ 0 * 3 ^ p3)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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1state_update components_23 (state_23 1 (3 ^ (p3 - 1))) three (3 ^ (p3 - 1) - 3 ^ (p3 - 1)) = state10p3: 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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1Some (3 * 3 ^ (p3 - 1)) = Some (2 ^ 0 * 3 ^ p3)by f_equal; 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: 1 ≤ 0 + p3
Hp3: p3 >= 0
n: p3 ≠ 0
n0: p3 ≠ 1Some (3 * 3 ^ (p3 - 1)) = Some (2 ^ 0 * 3 ^ Z.succ (p3 - 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 ≠ 0valid_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 ≠ 1valid_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 ≠ 1can_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 ≠ 1input_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 ≠ 1valid_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 ≠ 1option_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 ≠ 12 ≤ 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 ≠ 12 ^ (p2 - 1) ≤ state_23 (2 ^ (p2 - 1)) 1 twop2: 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 ≠ 1transition (existT two multiply_label) (state_23 (2 ^ (p2 - 1)) 1, Some (2 ^ (p2 - 1))) = (state01, Some (2 ^ p2 * 3 ^ 0))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 ≠ 1valid_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 ≠ 1option_valid_message_prop free_composition_23 (Some (2 ^ (p2 - 1)))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 ≠ 1option_valid_message_prop free_composition_23 (Some (2 ^ (p2 - 1) * 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 ≠ 12 ≤ 2 ^ (p2 - 1)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 ≠ 12 ≤ 2 ^ Z.succ (p2 - 2)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 ≠ 12 ^ (p2 - 1) ≤ state_23 (2 ^ (p2 - 1)) 1 twop2: 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 ≠ 1transition (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 ≠ 1state_update components_23 (state_23 (2 ^ (p2 - 1)) 1) two (2 ^ (p2 - 1) - 2 ^ (p2 - 1)) = state01p2: 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 ≠ 1Some (2 * 2 ^ (p2 - 1)) = Some (2 ^ p2 * 3 ^ 0)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 ≠ 1state_update components_23 (state_23 (2 ^ (p2 - 1)) 1) two (2 ^ (p2 - 1) - 2 ^ (p2 - 1)) = state01p2: 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 ≠ 1Some (2 * 2 ^ (p2 - 1)) = Some (2 ^ p2 * 3 ^ 0)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
n0: p2 ≠ 1Some (2 * 2 ^ (p2 - 1)) = Some (2 ^ Z.succ (p2 - 1) * 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 ≠ 0valid_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 ≠ 0can_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 ≠ 0input_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 ≠ 0valid_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 ≠ 0option_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 ≠ 02 ≤ 2 ^ (p2 - 1) * 3 ^ p3p2, 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 ≠ 02 ^ (p2 - 1) * 3 ^ p3 ≤ state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1 twop2, 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 ≠ 0transition (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3)) = (state01, Some (2 ^ p2 * 3 ^ p3))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 ≠ 0valid_state_prop free_composition_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1)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 ≠ 0option_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 ≠ 02 ≤ 2 ^ (p2 - 1) * 3 ^ p3by 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 ≠ 02 ≤ 2 ^ (p2 - 1) * 3 ^ Z.succ (p3 - 1)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 ≠ 02 ^ (p2 - 1) * 3 ^ p3 ≤ state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1 twop2, 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 ≠ 0transition (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 ≠ 0state_update components_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1) two (2 ^ (p2 - 1) * 3 ^ p3 - 2 ^ (p2 - 1) * 3 ^ p3) = state01p2, 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 ≠ 0Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ p2 * 3 ^ p3)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 ≠ 0state_update components_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1) two (2 ^ (p2 - 1) * 3 ^ p3 - 2 ^ (p2 - 1) * 3 ^ p3) = state01p2, 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 ≠ 0Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ p2 * 3 ^ p3)by f_equal; rewrite Z.pow_succ_r; lia. Qed.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 ≠ 0Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ Z.succ (p2 - 1) * 3 ^ p3)
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_messagevalid_message_prop free_composition_23 m → ∃ p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3m: multiplying_message(∃ p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3) → valid_message_prop free_composition_23 mby apply free_composition_23_valid_messages_powers_of_23_right.m: multiplying_messagevalid_message_prop free_composition_23 m → ∃ p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3m: multiplying_message(∃ p2 p3 : Z, p2 >= 0 ∧ p3 >= 0 ∧ p2 + p3 >= 1 ∧ m = 2 ^ p2 * 3 ^ p3) → valid_message_prop free_composition_23 mby 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.x, x0: Z
H: x >= 0
H0: x0 >= 0
H1: x + x0 >= 1valid_message_prop free_composition_23 (2 ^ x * 3 ^ x0)s: composite_state components_23
i: index23
z: Zzproj state_update_23 i = zby unfold state_update_23; destruct i; cbn; rewrite decide_True. Qed.s: composite_state components_23
i: index23
z: Zzproj state_update_23 i = zs: composite_state components_23
i: index23
z: Z∀ j : index23, j ≠ i → state_update_23 j = s jby intros; unfold state_update_23; rewrite decide_False. Qed. End sec_state_update_23_def.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' : 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) (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
z: Zstate_update_23 s two z = state_update components_23 s two zs: composite_state components_23
z: Zstate_update_23 s two z = state_update components_23 s two zs: composite_state components_23
z: Z(if decide (two = two) then z else s two) = zs: composite_state components_23
z: Z(if decide (two = three) then z else s three) = s threeby rewrite decide_True.s: composite_state components_23
z: Z(if decide (two = two) then z else s two) = zby rewrite decide_False. Qed.s: composite_state components_23
z: Z(if decide (two = three) then z else s three) = s threes: composite_state components_23
z: Zstate_update_23 s three z = state_update components_23 s three zs: composite_state components_23
z: Zstate_update_23 s three z = state_update components_23 s three zs: composite_state components_23
z: Z(if decide (three = two) then z else s two) = s twos: composite_state components_23
z: Z(if decide (three = three) then z else s three) = zby rewrite decide_False.s: composite_state components_23
z: Z(if decide (three = two) then z else s two) = s twoby rewrite decide_True. Qed.s: composite_state components_23
z: Z(if decide (three = three) then z else s three) = zi: index23composite_label components_23i: index23composite_label components_23by destruct i; exact (). Defined. Definition multiplier_23 (i : index23) : Z := match i with | two => 2 | three => 3 end.i: index23label (components_23 i)∀ 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 iin_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 → PropP sii: 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 iin_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 ≤ siin_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 = 3in_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 ≠ 3in_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 ≤ siin_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' iby 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))valid_state_prop free_composition_23 s'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)
H: input_valid_transition free_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))si - 2 = zproj s' ii: 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))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)option_valid_message_prop free_composition_23 (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)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))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 twostate_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 threestate_update_23 s three (s three - 2) = state_update components_23 s three (s three - 2)by apply state_update_23_two.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 twostate_update_23 s two (s two - 2) = state_update components_23 s two (s two - 2)by apply state_update_23_three.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 threestate_update_23 s three (s three - 2) = state_update components_23 s three (s three - 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
e: si = 3in_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 = 3input_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 = 3option_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 = 3valid (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 = 3transition (label_23 i) (s, Some 3) = (state_update_23 s i 0, Some (3 * multiplier_23 i))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 = 3option_valid_message_prop free_composition_23 (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 = 3valid (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 = 3transition (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 twostate_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 threestate_update_23 s three 0 = state_update components_23 s three (s three - 3)by rewrite state_update_23_two; f_equal; lia.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 twostate_update_23 s two 0 = state_update components_23 s two (s two - 3)by rewrite state_update_23_three; 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 threestate_update_23 s three 0 = state_update components_23 s three (s three - 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
n0: si ≠ 3in_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 ≠ 3input_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 ≠ 3option_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 ≠ 3valid (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 ≠ 3transition (label_23 i) (s, Some 2) = (state_update_23 s i 0, Some (2 * multiplier_23 i))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 ≠ 3option_valid_message_prop free_composition_23 (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 ≠ 3valid (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 ≠ 3transition (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 twostate_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 threestate_update_23 s three 0 = state_update components_23 s three (s three - 2)by rewrite state_update_23_two; f_equal; lia.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 twostate_update_23 s two 0 = state_update components_23 s two (s two - 2)by rewrite state_update_23_three; f_equal; lia. Qed.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 threestate_update_23 s three 0 = state_update components_23 s three (s three - 2)
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) state00s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3in_futures free_composition_23 (state_23 s2 s3) state00s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3) → in_futures free_composition_23 (state_23 s2 s3) state00s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3) → in_futures free_composition_23 (state_23 s2 s3) state00s2, 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) state00s2, 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 = state00s2, 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)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)valid_state_prop free_composition_23 (state_23 0 s3)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 = state00s2, 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 = 0s2, 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 = 0by 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 two = 0by rewrite state_update_23_three; state_update_simpl.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 = 0s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3in_futures free_composition_23 (state_23 s2 s3) (state_23 0 s3)s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3in_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 ≤ s3state_update_23 (state_23 s2 s3) two 0 = state_23 0 s3s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3in_futures free_composition_23 (state_23 s2 s3) (state_update_23 (state_23 s2 s3) two 0)by apply initial_state_is_valid; intros []; cbn; red; lia.s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3valid_state_prop free_composition_23 (state_23 s2 s3)s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3state_update_23 (state_23 s2 s3) two 0 = state_23 0 s3s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3state_update_23 (state_23 s2 s3) two 0 two = 0s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3state_update_23 (state_23 s2 s3) two 0 three = s3by rewrite state_update_23_two; state_update_simpl.s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3state_update_23 (state_23 s2 s3) two 0 two = 0by 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.s2, s3: Z
H: 2 ≤ s2
H0: 2 ≤ s3state_update_23 (state_23 s2 s3) two 0 three = s3l: composite_label components_23
s: composite_state components_23
m: multiplying_messageparity_constraint_23 l (s, Some m) ↔ Z.Even ml: composite_label components_23
s: composite_state components_23
m: multiplying_messageparity_constraint_23 l (s, Some m) ↔ Z.Even mby split; intros [n Hn]; destruct l as [[] li]; cbn in *; state_update_simpl; exists (s two + s three - n); lia. Qed.l: composite_label components_23
s: composite_state components_23
m: multiplying_messageZ.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∀ 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 omis_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 omis_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 omis_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 mm = 3 ∨ (∃ p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)by right; exists 1, 0; split; lia.s: composite_state components_23
Hs: composite_initial_state_prop components_23 s
x: multiplying_message
i: x = 2x = 3 ∨ (∃ p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ x = 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
_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 ^ p3s: 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 ^ p3s: 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 ^ p3s: 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 ^ p3s: 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: 2 ≤ 3 ≤ 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 >= 0 ∧ 2 * 3 = 2 ^ p2 * 3 ^ p3s: 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 >= 0 ∧ 2 * m = 2 ^ p2 * 3 ^ p3s: 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: 2 ≤ 3 ≤ 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 >= 0 ∧ 3 * 3 = 2 ^ p2 * 3 ^ p3s: 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 >= 0 ∧ 3 * m = 2 ^ p2 * 3 ^ p3by 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
Hc: Z.Even (composite_state_23_sum s + composite_state_23_sum (state_update components_23 s two (s two - 3)))
Hv: 2 ≤ 3 ≤ 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 >= 0 ∧ 2 * 3 = 2 ^ p2 * 3 ^ p3s: 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 >= 0 ∧ 2 * m = 2 ^ p2 * 3 ^ p3by 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
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 ^ p3p3 >= 0 ∧ 2 * m = 2 ^ Z.succ p2 * 3 ^ p3s: 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: 2 ≤ 3 ≤ 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 >= 0 ∧ 3 * 3 = 2 ^ p2 * 3 ^ p3s: 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)))Falseby state_update_simpl; lia.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 * nFalses: 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 >= 0 ∧ 3 * m = 2 ^ p2 * 3 ^ p3s: 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 ^ p3p2 >= 1 ∧ Z.succ p3 >= 0 ∧ 3 * m = 2 ^ p2 * 3 ^ Z.succ p3by rewrite Z.pow_succ_r; lia. Qed.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 ^ p3Z.succ p3 >= 0 ∧ 3 * m = 2 ^ p2 * 3 ^ Z.succ p3∀ 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 → PropP 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: 1 ≤ 1
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: 1 ≤ 1
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: 1 ≤ 1∀ 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: 1 ≤ 1
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: 1 ≤ 1
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: 1 ≤ 1
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: 1 ≤ 1
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: 1 ≤ 1
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: 1 ≤ 1
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)2 ≤ 2 ^ 1 * 3 ^ p3Hp2: 1 ≤ 1
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) threeHp2: 1 ≤ 1
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: 1 ≤ 1
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))by apply initial_state_is_valid; intros []; cbn; red; lia.Hp2: 1 ≤ 1
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))done.Hp2: 1 ≤ 1
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))by lia.Hp2: 1 ≤ 1
p3: Z
Hp3: 0 ≤ p3
Hind: valid_message_prop parity_composition_23 (2 ^ 1 * 3 ^ p3)2 ≤ 2 ^ 1 * 3 ^ p3by cbn; lia.Hp2: 1 ≤ 1
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) threeby apply parity_constraint_23_even; exists (3 ^ p3); lia.Hp2: 1 ≤ 1
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: 1 ≤ 1
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: 1 ≤ 1
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) = state10Hp2: 1 ≤ 1
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 extensionality i; destruct i; state_update_simpl; cbn; lia.Hp2: 1 ≤ 1
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) = state10by f_equal; rewrite Z.pow_succ_r; lia.Hp2: 1 ≤ 1
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)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 ≤ p3valid_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 ≤ p3can_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 ≤ p3input_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 ≤ p3valid_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 ≤ p3option_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 ≤ p32 ≤ 2 ^ (p2 - 1) * 3 ^ p3p2: 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 ≤ p32 ^ (p2 - 1) * 3 ^ p3 ≤ state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1 twop2: 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 ≤ p3parity_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 ≤ p3transition (existT two multiply_label) (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1, Some (2 ^ (p2 - 1) * 3 ^ p3)) = (state01, Some (2 ^ p2 * 3 ^ p3))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 ≤ p3valid_state_prop parity_composition_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1)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 ≤ p3option_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 ≤ p32 ≤ 2 ^ (p2 - 1) * 3 ^ p3by 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 ≤ p32 ≤ 2 ^ Z.succ (p2 - 2) * 3 ^ p3by 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 ≤ p32 ^ (p2 - 1) * 3 ^ p3 ≤ state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1 twop2: 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 ≤ p3parity_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 ≤ p32 ^ (p2 - 1) * 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 ≤ p32 ^ Z.succ (p2 - 2) * 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 ≤ p3transition (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 ≤ p3state_update components_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1) two (2 ^ (p2 - 1) * 3 ^ p3 - 2 ^ (p2 - 1) * 3 ^ p3) = state01p2: 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 ≤ p3Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ p2 * 3 ^ p3)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 ≤ p3state_update components_23 (state_23 (2 ^ (p2 - 1) * 3 ^ p3) 1) two (2 ^ (p2 - 1) * 3 ^ p3 - 2 ^ (p2 - 1) * 3 ^ p3) = state01p2: 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 ≤ p3Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ p2 * 3 ^ p3)by f_equal; rewrite !Z.pow_succ_r; lia. Qed.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 ≤ p3Some (2 * (2 ^ (p2 - 1) * 3 ^ p3)) = Some (2 ^ Z.succ (p2 - 1) * 3 ^ p3)
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_messagevalid_message_prop parity_composition_23 m → m = 3 ∨ (∃ p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)m: multiplying_messagem = 3 ∨ (∃ p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3) → valid_message_prop parity_composition_23 mby apply parity_composition_23_valid_messages_powers_of_23_right.m: multiplying_messagevalid_message_prop parity_composition_23 m → m = 3 ∨ (∃ p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3)m: multiplying_messagem = 3 ∨ (∃ p2 p3 : Z, p2 >= 1 ∧ p3 >= 0 ∧ m = 2 ^ p2 * 3 ^ p3) → valid_message_prop parity_composition_23 mvalid_message_prop parity_composition_23 3x, x0: Z
H: x >= 1
H0: x0 >= 0valid_message_prop parity_composition_23 (2 ^ x * 3 ^ x0)by apply initial_message_is_valid, composition_23_3_initial.valid_message_prop parity_composition_23 3by apply parity_composition_23_valid_messages_powers_of_23_left; lia. Qed.x, x0: Z
H: x >= 1
H0: x0 >= 0valid_message_prop parity_composition_23 (2 ^ x * 3 ^ x0)
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 >= 1valid_state_prop parity_composition_23 (state_23 n m)by apply initial_state_is_valid; intros []; cbn; red. Qed.n, m: Z
Hn: n >= 1
Hm: m >= 1valid_state_prop parity_composition_23 (state_23 n m)valid_state_prop parity_composition_23 state11by apply (valid_state_23_geq1 1 1); lia. Qed.valid_state_prop parity_composition_23 state11valid_state_prop parity_composition_23 state22by apply valid_state_23_geq1. Qed.valid_state_prop parity_composition_23 state22n: Z
Hn: n >= 1valid_state_prop parity_composition_23 (state_23 0 n)n: Z
Hn: n >= 1valid_state_prop parity_composition_23 (state_23 0 n)n: Z
Hn: n >= 1input_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 >= 1valid_state_prop parity_composition_23 (state_23 2 n)n: Z
Hn: n >= 1option_valid_message_prop parity_composition_23 (Some 2)n: Z
Hn: n >= 12 ≤ 2n: Z
Hn: n >= 12 ≤ state_23 2 n twon: Z
Hn: n >= 1parity_constraint_23 (existT two multiply_label) (state_23 2 n, Some 2)n: Z
Hn: n >= 1transition (existT two multiply_label) (state_23 2 n, Some 2) = (state_23 0 n, Some 4)by apply valid_state_23_geq1.n: Z
Hn: n >= 1valid_state_prop parity_composition_23 (state_23 2 n)by apply initial_message_is_valid, composition_23_2_initial.n: Z
Hn: n >= 1option_valid_message_prop parity_composition_23 (Some 2)by lia.n: Z
Hn: n >= 12 ≤ 2by cbn; lia.n: Z
Hn: n >= 12 ≤ state_23 2 n twoby apply parity_constraint_23_even; exists 1; lia.n: Z
Hn: n >= 1parity_constraint_23 (existT two multiply_label) (state_23 2 n, Some 2)by cbn; f_equal; extensionality i; destruct i; cbn; state_update_simpl; cbn. Qed.n: Z
Hn: n >= 1transition (existT two multiply_label) (state_23 2 n, Some 2) = (state_23 0 n, Some 4)n: Z
Hn: n >= 1valid_state_prop parity_composition_23 (state_23 n 0)n: Z
Hn: n >= 1valid_state_prop parity_composition_23 (state_23 n 0)n: Z
Hn: n >= 1input_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 >= 1valid_state_prop parity_composition_23 (state_23 n 2)n: Z
Hn: n >= 1option_valid_message_prop parity_composition_23 (Some 2)n: Z
Hn: n >= 12 ≤ 2n: Z
Hn: n >= 12 ≤ state_23 n 2 threen: Z
Hn: n >= 1parity_constraint_23 (existT three multiply_label) (state_23 n 2, Some 2)n: Z
Hn: n >= 1transition (existT three multiply_label) (state_23 n 2, Some 2) = (state_23 n 0, Some 6)by apply valid_state_23_geq1.n: Z
Hn: n >= 1valid_state_prop parity_composition_23 (state_23 n 2)by apply initial_message_is_valid, composition_23_2_initial.n: Z
Hn: n >= 1option_valid_message_prop parity_composition_23 (Some 2)by lia.n: Z
Hn: n >= 12 ≤ 2by cbn; lia.n: Z
Hn: n >= 12 ≤ state_23 n 2 threeby apply parity_constraint_23_even; exists 1; lia.n: Z
Hn: n >= 1parity_constraint_23 (existT three multiply_label) (state_23 n 2, Some 2)cbn; f_equal; extensionality i; destruct i; cbn; state_update_simpl; cbn; lia. Qed.n: Z
Hn: n >= 1transition (existT three multiply_label) (state_23 n 2, Some 2) = (state_23 n 0, Some 6)valid_state_prop parity_composition_23 state00valid_state_prop parity_composition_23 state00input_valid_transition parity_composition_23 (existT three multiply_label) (state02, Some 2) (state00, Some 6)valid_state_prop parity_composition_23 state02option_valid_message_prop parity_composition_23 (Some 2)2 ≤ 22 ≤ state02 threeparity_constraint_23 (existT three multiply_label) (state02, Some 2)transition (existT three multiply_label) (state02, Some 2) = (state00, Some 6)by apply valid_state0n.valid_state_prop parity_composition_23 state02by apply initial_message_is_valid, composition_23_2_initial.option_valid_message_prop parity_composition_23 (Some 2)by lia.2 ≤ 2by unfold state02; cbn; lia.2 ≤ state02 threeby red; cbn; unfold composite_state_23_sum; state_update_simpl; cbn; exists 1.parity_constraint_23 (existT three multiply_label) (state02, Some 2)by cbn; f_equal; extensionality i; destruct i; cbn; state_update_simpl; cbn. Qed.transition (existT three multiply_label) (state02, Some 2) = (state00, Some 6)valid_state_prop parity_composition_23 state01by apply valid_state0n. Qed.valid_state_prop parity_composition_23 state01valid_state_prop parity_composition_23 state10by apply valid_staten0. Qed.valid_state_prop parity_composition_23 state10s: composite_state components_23s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11 → parity_23_final_state ss: composite_state components_23s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11 → parity_23_final_state ss: composite_state components_23
Hcases: s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11parity_23_final_state ss: composite_state components_23
Hcases: s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11valid_state_prop parity_composition_23 ss: 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 = state11valid_state_prop parity_composition_23 svalid_state_prop parity_composition_23 state00valid_state_prop parity_composition_23 state01valid_state_prop parity_composition_23 state10valid_state_prop parity_composition_23 state11by apply valid_state00.valid_state_prop parity_composition_23 state00by apply valid_state01.valid_state_prop parity_composition_23 state01by apply valid_state10.valid_state_prop parity_composition_23 state10by apply valid_state11.valid_state_prop parity_composition_23 state11s: 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)Falseby 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
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 * nFalse∀ 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 >= 0s': 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 >= 0s': 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 >= 0by destruct j; (destruct om ; [| done]); inversion Ht; subst; clear Ht; cbn in *; destruct i; cbn in *; state_update_simpl; lia. Qed.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 >= 0zproj s' i >= 0s: composite_state components_23parity_23_final_state s → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11s: composite_state components_23parity_23_final_state s → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11s: 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 = state11s: 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 = state11s: 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 = 1s: 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 = state11s: 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 = 0s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11s: 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 = 1s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11s: 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 = 0s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11s: 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 = 1s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11by 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 = 0s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11by 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 = 0
H0: s three = 1s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11by 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 = 0s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11by 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')
H: s two = 1
H0: s three = 1s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11s: 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 = 1s: 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 = 1s: 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 > 1s: 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 > 1s: 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 >= 0s two > 1 ∨ s three > 1by 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)
H: zproj s two >= 0
H0: zproj s three >= 0s two > 1 ∨ s three > 1s: 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 > 1input_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 > 1option_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 > 12 ≤ 2s: 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 > 12 ≤ s twos: 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 > 1parity_constraint_23 (existT two ()) (s, 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 > 1option_valid_message_prop parity_composition_23 (Some 2)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 > 12 ≤ 2by 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 > 12 ≤ s twoby 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 two > 1parity_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 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 > 1input_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 > 1option_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 > 12 ≤ 2s: 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 > 12 ≤ s threes: 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 > 1parity_constraint_23 (existT three ()) (s, 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 > 1option_valid_message_prop parity_composition_23 (Some 2)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 > 12 ≤ 2by 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 > 12 ≤ s threeby apply parity_constraint_23_even; exists 1; lia. Qed.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 > 1parity_constraint_23 (existT three ()) (s, Some 2)
The final states of the parity_composition_23 VLSM consist of
state00, state01, state10, and state11.
s: composite_state components_23parity_23_final_state s ↔ s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11s: composite_state components_23parity_23_final_state s ↔ s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11s: composite_state components_23parity_23_final_state s → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11s: composite_state components_23s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11 → parity_23_final_state sby apply parity_23_final_state_prop23_right.s: composite_state components_23parity_23_final_state s → s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11by apply parity_23_final_state_prop23_left. Qed.s: composite_state components_23s = state00 ∨ s = state01 ∨ s = state10 ∨ s = state11 → parity_23_final_state s∀ 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 ≤ nzproj 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 → PropP ni: 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 ni: 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 * 0in_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 * 0state_update_23 s i 0 = ss: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s two = 2 * 0state_update_23 s two 0 = ss: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s three = 2 * 0state_update_23 s three 0 = sby rewrite state_update_23_two, state_update_id.s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s two = 2 * 0state_update_23 s two 0 = sby rewrite state_update_23_three, state_update_id.s: composite_state components_23
Hs: valid_state_prop parity_composition_23 s
Hsi: zproj s three = 2 * 0state_update_23 s three 0 = si: 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 nin_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 * nby 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))valid_state_prop parity_composition_23 s'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)
H: input_valid_transition parity_composition_23 (label_23 i) (s, Some 2) (s', Some (2 * multiplier_23 i))zproj s' i = 2 * ni: 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))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)option_valid_message_prop parity_composition_23 (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)valid (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)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))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)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 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_three. Qed.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)
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)) state00s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) state00s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3in_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)) state00s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3in_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)) state00s2, 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)) state00s2, 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 = state00s2, 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)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))valid_state_prop parity_composition_23 (state_23 0 (2 * s3))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 = state00s2, 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 = 0s2, 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 = 0by 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 two = 0by rewrite state_update_23_three; state_update_simpl.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 = 0s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3in_futures parity_composition_23 (state_23 (2 * s2) (2 * s3)) (state_23 0 (2 * s3))s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3in_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 ≤ s3state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 = state_23 0 (2 * s3)s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3in_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 ≤ s3valid_state_prop parity_composition_23 (state_23 (2 * s2) (2 * s3))H, H0: 0 ≤ 0valid_state_prop parity_composition_23 (state_23 (2 * 0) (2 * 0))s3: Z
H: 0 ≤ 0
H0: 0 ≤ s3
n: s3 ≠ 0valid_state_prop parity_composition_23 (state_23 (2 * 0) (2 * s3))s2: Z
H: 0 ≤ s2
H0: 0 ≤ 0
n: s2 ≠ 0valid_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 ≠ 0valid_state_prop parity_composition_23 (state_23 (2 * s2) (2 * s3))by apply valid_state00.H, H0: 0 ≤ 0valid_state_prop parity_composition_23 (state_23 (2 * 0) (2 * 0))by apply valid_state0n; lia.s3: Z
H: 0 ≤ 0
H0: 0 ≤ s3
n: s3 ≠ 0valid_state_prop parity_composition_23 (state_23 (2 * 0) (2 * s3))by apply valid_staten0; lia.s2: Z
H: 0 ≤ s2
H0: 0 ≤ 0
n: s2 ≠ 0valid_state_prop parity_composition_23 (state_23 (2 * s2) (2 * 0))by apply valid_state_23_geq1; lia.s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3
n: s2 ≠ 0
n0: s3 ≠ 0valid_state_prop parity_composition_23 (state_23 (2 * s2) (2 * s3))s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 = state_23 0 (2 * s3)s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 two = 0s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 three = 2 * s3by rewrite state_update_23_two; state_update_simpl.s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 two = 0by rewrite state_update_23_neq. Qed. End sec_23_composition.s2, s3: Z
H: 0 ≤ s2
H0: 0 ≤ s3state_update_23 (state_23 (2 * s2) (2 * s3)) two 0 three = 2 * s3