Signed weighted sums and linearity — exact evidence

Current Alpha v34 checked use; first admitted v31; not Stable. Original HA and the independently compiled Lean checker have freshly verified the complete bundle before this page was generated.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

227 checked bundle nodes · 584 proof edges · 13692 body proof nodes.

Literal self-contained proof bundle · SHA-256 e88ddec495a71d673e670299ea3943a5a996eecb1296fb746e107c8e0b81c967

signed_sum_linearity_candidate.py · signed_table_operations_candidate.py · signed_weighted_sum_candidate.py

Unchanged historical local checkpoint record · Historical snapshot manifest. Those records retain their original non-admitting flags; current authority comes from the separate freshly verified v31 release.

Exact theorem nodes and inherited prerequisites

WS0001 signed_table_domain_resize · actual bundle node 186
WS0002 signed_table_lookup_any · actual bundle node 187
WS0003 signed_table_add_lookup · actual bundle node 188
WS0004 signed_table_add_restrict · actual bundle node 189
WS0005 signed_table_add_empty · actual bundle node 190
WS0006 signed_table_add_extensional_unique · actual bundle node 191
WS0007 signed_table_multiply_lookup · actual bundle node 192
WS0008 signed_table_multiply_restrict · actual bundle node 193
WS0009 signed_table_multiply_empty · actual bundle node 194
WS000A signed_table_multiply_extensional_unique · actual bundle node 195
WS000B signed_table_scalar_lookup · actual bundle node 196
WS000C signed_table_scalar_restrict · actual bundle node 197
WS000D signed_table_scalar_empty · actual bundle node 198
WS000E signed_table_scalar_extensional_unique · actual bundle node 199
WS000F signed_table_add_extend · actual bundle node 200
WS0010 signed_table_add_exists · actual bundle node 201
WS0011 signed_table_add_exists_extensionally_unique · actual bundle node 202
WS0012 signed_table_multiply_extend · actual bundle node 203
WS0013 signed_table_multiply_exists · actual bundle node 204
WS0014 signed_table_multiply_exists_extensionally_unique · actual bundle node 205
WS0015 signed_table_scalar_extend · actual bundle node 206
WS0016 signed_table_scalar_exists · actual bundle node 207
WS0017 signed_table_scalar_exists_extensionally_unique · actual bundle node 208
WS0018 signed_table_add_reassociate · actual bundle node 209
WS0019 signed_table_add_medial · actual bundle node 210
WS001A signed_table_scalar_add_intro · actual bundle node 211
WS001B signed_prefix_sum_pointwise_add · actual bundle node 212
WS001C signed_prefix_sum_scalar_multiply · actual bundle node 213
WS001D signed_prefix_sum_pointwise_add_values_exist · actual bundle node 214
WS001E signed_prefix_sum_scalar_multiply_values_exist · actual bundle node 215
WS001F signed_weighted_sum_exists · actual bundle node 216
WS0020 signed_weighted_sum_functional · actual bundle node 217
WS0021 signed_weighted_sum_exists_unique · actual bundle node 218
WS0022 signed_weighted_sum_empty_value · actual bundle node 219
WS0023 signed_weighted_sum_empty_exists · actual bundle node 220
WS0024 signed_table_weighted_add_distributive · actual bundle node 221
WS0025 signed_weighted_scalar_commute · actual bundle node 222
WS0026 signed_table_weighted_scalar_commute · actual bundle node 223
WS0027 signed_weighted_sum_add_linearity · actual bundle node 224
WS0028 signed_weighted_sum_scalar_linearity · actual bundle node 225
add_eq_zero_right · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. a + b = 0 -> b = 0
```

arithmetic_signed_sum_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F l. (exists dst_positive_code_sum_exists_input dst_positive_scale_sum_exists_input dst_negative_code_sum_exists_input dst_negative_scale_sum_exists_input. (((F) = (((((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) * S ((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) + ((dst_positive_scale_sum_exists_input) + (dst_positive_scale_sum_exists_input))) + (((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input)))) * S ((((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) * S ((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) + ((dst_positive_scale_sum_exists_input) + (dst_positive_scale_sum_exists_input))) + (((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input)))) + ((((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input))) + (((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input)))))) /\ (forall dst_index_sum_exists_input. (exists pvs_le_gap_sum_exists_inputdomain. pvs_le_gap_sum_exists_inputdomain + (dst_index_sum_exists_input) = (N)) -> exists dst_positive_sum_exists_input dst_negative_sum_exists_input dst_value_sum_exists_input. ((((exists ff_h_pvs_sum_exists_inputentrypositive. ff_h_pvs_sum_exists_inputentrypositive + S (dst_positive_sum_exists_input) = S ((S (dst_index_sum_exists_input)) * dst_positive_scale_sum_exists_input)) /\ exists ff_q_pvs_sum_exists_inputentrypositive. dst_positive_code_sum_exists_input = ff_q_pvs_sum_exists_inputentrypositive * S ((S (dst_index_sum_exists_input)) * dst_positive_scale_sum_exists_input) + (dst_positive_sum_exists_input))) /\ (((((exists ff_h_pvs_sum_exists_inputentrynegative. ff_h_pvs_sum_exists_inputentrynegative + S (dst_negative_sum_exists_input) = S ((S (dst_index_sum_exists_input)) * dst_negative_scale_sum_exists_input)) /\ exists ff_q_pvs_sum_exists_inputentrynegative. dst_negative_code_sum_exists_input = ff_q_pvs_sum_exists_inputentrynegative * S ((S (dst_index_sum_exists_input)) * dst_negative_scale_sum_exists_input) + (dst_negative_sum_exists_input))) /\ (exists ge_balance_positive_sum_exists_inputentryvalue ge_balance_negative_sum_exists_inputentryvalue. (((((dst_value_sum_exists_input) = 2 * (ge_balance_positive_sum_exists_inputentryvalue) /\ (ge_balance_negative_sum_exists_inputentryvalue) = 0) \/ exists ge_signed_half_sum_exists_inputentryvaluedecode. (((dst_value_sum_exists_input) = 2 * ge_signed_half_sum_exists_inputentryvaluedecode + 1 /\ (ge_balance_positive_sum_exists_inputentryvalue) = 0) /\ (ge_balance_negative_sum_exists_inputentryvalue) = S ge_signed_half_sum_exists_inputentryvaluedecode))) /\ ((dst_positive_sum_exists_input) + ge_balance_negative_sum_exists_inputentryvalue = (dst_negative_sum_exists_input) + ge_balance_positive_sum_exists_inputentryvalue))))))))) -> exists z. (exists dst_positive_code_sum_exists_output dst_positive_scale_sum_exists_output dst_negative_code_sum_exists_output dst_negative_scale_sum_exists_output dst_positive_sum_sum_exists_output dst_negative_sum_sum_exists_output. (((F) = (((((dst_positive_code_sum_exists_output) + (dst_positive_scale_sum_exists_output)) * S ((dst_positive_code_sum_exists_output) + (dst_positive_scale_sum_exists_output)) + ((dst_positive_scale_sum_exists_output) + (dst_positive_scale_sum_exists_output))) + (((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) * S ((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) + ((dst_negative_scale_sum_exists_output) + (dst_negative_scale_sum_exists_output)))) * S ((((dst_positive_code_sum_exists_output) + (dst_positive_scale_sum_exists_output)) * S ((dst_positive_code_sum_exists_output) + (dst_positive_scale_sum_exists_output)) + ((dst_positive_scale_sum_exists_output) + (dst_positive_scale_sum_exists_output))) + (((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) * S ((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) + ((dst_negative_scale_sum_exists_output) + (dst_negative_scale_sum_exists_output)))) + ((((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) * S ((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) + ((dst_negative_scale_sum_exists_output) + (dst_negative_scale_sum_exists_output))) + (((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) * S ((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) + ((dst_negative_scale_sum_exists_output) + (dst_negative_scale_sum_exists_output)))))) /\ (((exists fs_u_dst_sum_exists_outputpositive fs_v_dst_sum_exists_outputpositive. ((((exists fs_h_dst_sum_exists_outputpositive_body_start. fs_h_dst_sum_exists_outputpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_exists_outputpositive)) /\ exists fs_q_dst_sum_exists_outputpositive_body_start. fs_u_dst_sum_exists_outputpositive = fs_q_dst_sum_exists_outputpositive_body_start * S ((S (0)) * fs_v_dst_sum_exists_outputpositive) + (0))) /\ ((((exists fs_h_dst_sum_exists_outputpositive_body_terminal. fs_h_dst_sum_exists_outputpositive_body_terminal + S (dst_positive_sum_sum_exists_output) = S ((S (l)) * fs_v_dst_sum_exists_outputpositive)) /\ exists fs_q_dst_sum_exists_outputpositive_body_terminal. fs_u_dst_sum_exists_outputpositive = fs_q_dst_sum_exists_outputpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_exists_outputpositive) + (dst_positive_sum_sum_exists_output))) /\ forall fs_i_dst_sum_exists_outputpositive_body_steps. (exists fs_lt_dst_sum_exists_outputpositive_body_steps_bound. fs_lt_dst_sum_exists_outputpositive_body_steps_bound + S fs_i_dst_sum_exists_outputpositive_body_steps = l) -> exists fs_a_dst_sum_exists_outputpositive_body_steps fs_r_dst_sum_exists_outputpositive_body_steps fs_s_dst_sum_exists_outputpositive_body_steps. ((((exists fs_h_dst_sum_exists_outputpositive_body_steps_summand. fs_h_dst_sum_exists_outputpositive_body_steps_summand + S (fs_a_dst_sum_exists_outputpositive_body_steps) = S ((S (fs_i_dst_sum_exists_outputpositive_body_steps)) * dst_positive_scale_sum_exists_output)) /\ exists fs_q_dst_sum_exists_outputpositive_body_steps_summand. dst_positive_code_sum_exists_output = fs_q_dst_sum_exists_outputpositive_body_steps_summand * S ((S (fs_i_dst_sum_exists_outputpositive_body_steps)) * dst_positive_scale_sum_exists_output) + (fs_a_dst_sum_exists_outputpositive_body_steps))) /\ ((((exists fs_h_dst_sum_exists_outputpositive_body_steps_partial. fs_h_dst_sum_exists_outputpositive_body_steps_partial + S (fs_r_dst_sum_exists_outputpositive_body_steps) = S ((S (fs_i_dst_sum_exists_outputpositive_body_steps)) * fs_v_dst_sum_exists_outputpositive)) /\ exists fs_q_dst_sum_exists_outputpositive_body_steps_partial. fs_u_dst_sum_exists_outputpositive = fs_q_dst_sum_exists_outputpositive_body_steps_partial * S ((S (fs_i_dst_sum_exists_outputpositive_body_steps)) * fs_v_dst_sum_exists_outputpositive) + (fs_r_dst_sum_exists_outputpositive_body_steps))) /\ ((((exists fs_h_dst_sum_exists_outputpositive_body_steps_successor. fs_h_dst_sum_exists_outputpositive_body_steps_successor + S (fs_s_dst_sum_exists_outputpositive_body_steps) = S ((S (S fs_i_dst_sum_exists_outputpositive_body_steps)) * fs_v_dst_sum_exists_outputpositive)) /\ exists fs_q_dst_sum_exists_outputpositive_body_steps_successor. fs_u_dst_sum_exists_outputpositive = fs_q_dst_sum_exists_outputpositive_body_steps_successor * S ((S (S fs_i_dst_sum_exists_outputpositive_body_steps)) * fs_v_dst_sum_exists_outputpositive) + (fs_s_dst_sum_exists_outputpositive_body_steps))) /\ fs_s_dst_sum_exists_outputpositive_body_steps = fs_r_dst_sum_exists_outputpositive_body_steps + fs_a_dst_sum_exists_outputpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_exists_outputnegative fs_v_dst_sum_exists_outputnegative. ((((exists fs_h_dst_sum_exists_outputnegative_body_start. fs_h_dst_sum_exists_outputnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_exists_outputnegative)) /\ exists fs_q_dst_sum_exists_outputnegative_body_start. fs_u_dst_sum_exists_outputnegative = fs_q_dst_sum_exists_outputnegative_body_start * S ((S (0)) * fs_v_dst_sum_exists_outputnegative) + (0))) /\ ((((exists fs_h_dst_sum_exists_outputnegative_body_terminal. fs_h_dst_sum_exists_outputnegative_body_terminal + S (dst_negative_sum_sum_exists_output) = S ((S (l)) * fs_v_dst_sum_exists_outputnegative)) /\ exists fs_q_dst_sum_exists_outputnegative_body_terminal. fs_u_dst_sum_exists_outputnegative = fs_q_dst_sum_exists_outputnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_exists_outputnegative) + (dst_negative_sum_sum_exists_output))) /\ forall fs_i_dst_sum_exists_outputnegative_body_steps. (exists fs_lt_dst_sum_exists_outputnegative_body_steps_bound. fs_lt_dst_sum_exists_outputnegative_body_steps_bound + S fs_i_dst_sum_exists_outputnegative_body_steps = l) -> exists fs_a_dst_sum_exists_outputnegative_body_steps fs_r_dst_sum_exists_outputnegative_body_steps fs_s_dst_sum_exists_outputnegative_body_steps. ((((exists fs_h_dst_sum_exists_outputnegative_body_steps_summand. fs_h_dst_sum_exists_outputnegative_body_steps_summand + S (fs_a_dst_sum_exists_outputnegative_body_steps) = S ((S (fs_i_dst_sum_exists_outputnegative_body_steps)) * dst_negative_scale_sum_exists_output)) /\ exists fs_q_dst_sum_exists_outputnegative_body_steps_summand. dst_negative_code_sum_exists_output = fs_q_dst_sum_exists_outputnegative_body_steps_summand * S ((S (fs_i_dst_sum_exists_outputnegative_body_steps)) * dst_negative_scale_sum_exists_output) + (fs_a_dst_sum_exists_outputnegative_body_steps))) /\ ((((exists fs_h_dst_sum_exists_outputnegative_body_steps_partial. fs_h_dst_sum_exists_outputnegative_body_steps_partial + S (fs_r_dst_sum_exists_outputnegative_body_steps) = S ((S (fs_i_dst_sum_exists_outputnegative_body_steps)) * fs_v_dst_sum_exists_outputnegative)) /\ exists fs_q_dst_sum_exists_outputnegative_body_steps_partial. fs_u_dst_sum_exists_outputnegative = fs_q_dst_sum_exists_outputnegative_body_steps_partial * S ((S (fs_i_dst_sum_exists_outputnegative_body_steps)) * fs_v_dst_sum_exists_outputnegative) + (fs_r_dst_sum_exists_outputnegative_body_steps))) /\ ((((exists fs_h_dst_sum_exists_outputnegative_body_steps_successor. fs_h_dst_sum_exists_outputnegative_body_steps_successor + S (fs_s_dst_sum_exists_outputnegative_body_steps) = S ((S (S fs_i_dst_sum_exists_outputnegative_body_steps)) * fs_v_dst_sum_exists_outputnegative)) /\ exists fs_q_dst_sum_exists_outputnegative_body_steps_successor. fs_u_dst_sum_exists_outputnegative = fs_q_dst_sum_exists_outputnegative_body_steps_successor * S ((S (S fs_i_dst_sum_exists_outputnegative_body_steps)) * fs_v_dst_sum_exists_outputnegative) + (fs_s_dst_sum_exists_outputnegative_body_steps))) /\ fs_s_dst_sum_exists_outputnegative_body_steps = fs_r_dst_sum_exists_outputnegative_body_steps + fs_a_dst_sum_exists_outputnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_exists_outputresult ge_balance_negative_sum_exists_outputresult. (((((z) = 2 * (ge_balance_positive_sum_exists_outputresult) /\ (ge_balance_negative_sum_exists_outputresult) = 0) \/ exists ge_signed_half_sum_exists_outputresultdecode. (((z) = 2 * ge_signed_half_sum_exists_outputresultdecode + 1 /\ (ge_balance_positive_sum_exists_outputresult) = 0) /\ (ge_balance_negative_sum_exists_outputresult) = S ge_signed_half_sum_exists_outputresultdecode))) /\ ((dst_positive_sum_sum_exists_output) + ge_balance_negative_sum_exists_outputresult = (dst_negative_sum_sum_exists_output) + ge_balance_positive_sum_exists_outputresult)))))))))

arithmetic_signed_table_equal_entry_transport · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F G l i z. (exists dst_positive_code_transport_valid dst_positive_scale_transport_valid dst_negative_code_transport_valid dst_negative_scale_transport_valid. (((G) = (((((dst_positive_code_transport_valid) + (dst_positive_scale_transport_valid)) * S ((dst_positive_code_transport_valid) + (dst_positive_scale_transport_valid)) + ((dst_positive_scale_transport_valid) + (dst_positive_scale_transport_valid))) + (((dst_negative_code_transport_valid) + (dst_negative_scale_transport_valid)) * S ((dst_negative_code_transport_valid) + (dst_negative_scale_transport_valid)) + ((dst_negative_scale_transport_valid) + (dst_negative_scale_transport_valid)))) * S ((((dst_positive_code_transport_valid) + (dst_positive_scale_transport_valid)) * S ((dst_positive_code_transport_valid) + (dst_positive_scale_transport_valid)) + ((dst_positive_scale_transport_valid) + (dst_positive_scale_transport_valid))) + (((dst_negative_code_transport_valid) + (dst_negative_scale_transport_valid)) * S ((dst_negative_code_transport_valid) + (dst_negative_scale_transport_valid)) + ((dst_negative_scale_transport_valid) + (dst_negative_scale_transport_valid)))) + ((((dst_negative_code_transport_valid) + (dst_negative_scale_transport_valid)) * S ((dst_negative_code_transport_valid) + (dst_negative_scale_transport_valid)) + ((dst_negative_scale_transport_valid) + (dst_negative_scale_transport_valid))) + (((dst_negative_code_transport_valid) + (dst_negative_scale_transport_valid)) * S ((dst_negative_code_transport_valid) + (dst_negative_scale_transport_valid)) + ((dst_negative_scale_transport_valid) + (dst_negative_scale_transport_valid)))))) /\ (forall dst_index_transport_valid. (exists pvs_le_gap_transport_validdomain. pvs_le_gap_transport_validdomain + (dst_index_transport_valid) = (N)) -> exists dst_positive_transport_valid dst_negative_transport_valid dst_value_transport_valid. ((((exists ff_h_pvs_transport_validentrypositive. ff_h_pvs_transport_validentrypositive + S (dst_positive_transport_valid) = S ((S (dst_index_transport_valid)) * dst_positive_scale_transport_valid)) /\ exists ff_q_pvs_transport_validentrypositive. dst_positive_code_transport_valid = ff_q_pvs_transport_validentrypositive * S ((S (dst_index_transport_valid)) * dst_positive_scale_transport_valid) + (dst_positive_transport_valid))) /\ (((((exists ff_h_pvs_transport_validentrynegative. ff_h_pvs_transport_validentrynegative + S (dst_negative_transport_valid) = S ((S (dst_index_transport_valid)) * dst_negative_scale_transport_valid)) /\ exists ff_q_pvs_transport_validentrynegative. dst_negative_code_transport_valid = ff_q_pvs_transport_validentrynegative * S ((S (dst_index_transport_valid)) * dst_negative_scale_transport_valid) + (dst_negative_transport_valid))) /\ (exists ge_balance_positive_transport_validentryvalue ge_balance_negative_transport_validentryvalue. (((((dst_value_transport_valid) = 2 * (ge_balance_positive_transport_validentryvalue) /\ (ge_balance_negative_transport_validentryvalue) = 0) \/ exists ge_signed_half_transport_validentryvaluedecode. (((dst_value_transport_valid) = 2 * ge_signed_half_transport_validentryvaluedecode + 1 /\ (ge_balance_positive_transport_validentryvalue) = 0) /\ (ge_balance_negative_transport_validentryvalue) = S ge_signed_half_transport_validentryvaluedecode))) /\ ((dst_positive_transport_valid) + ge_balance_negative_transport_validentryvalue = (dst_negative_transport_valid) + ge_balance_positive_transport_validentryvalue))))))))) -> (forall dst_index_transport_prefix dst_first_transport_prefix dst_second_transport_prefix. (exists pvs_gap_transport_prefixbound. pvs_gap_transport_prefixbound + S (dst_index_transport_prefix) = (l)) -> (exists dst_positive_code_transport_prefixfirst dst_positive_scale_transport_prefixfirst dst_negative_code_transport_prefixfirst dst_negative_scale_transport_prefixfirst dst_positive_transport_prefixfirst dst_negative_transport_prefixfirst. (((F) = (((((dst_positive_code_transport_prefixfirst) + (dst_positive_scale_transport_prefixfirst)) * S ((dst_positive_code_transport_prefixfirst) + (dst_positive_scale_transport_prefixfirst)) + ((dst_positive_scale_transport_prefixfirst) + (dst_positive_scale_transport_prefixfirst))) + (((dst_negative_code_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)) * S ((dst_negative_code_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)) + ((dst_negative_scale_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)))) * S ((((dst_positive_code_transport_prefixfirst) + (dst_positive_scale_transport_prefixfirst)) * S ((dst_positive_code_transport_prefixfirst) + (dst_positive_scale_transport_prefixfirst)) + ((dst_positive_scale_transport_prefixfirst) + (dst_positive_scale_transport_prefixfirst))) + (((dst_negative_code_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)) * S ((dst_negative_code_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)) + ((dst_negative_scale_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)))) + ((((dst_negative_code_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)) * S ((dst_negative_code_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)) + ((dst_negative_scale_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst))) + (((dst_negative_code_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)) * S ((dst_negative_code_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)) + ((dst_negative_scale_transport_prefixfirst) + (dst_negative_scale_transport_prefixfirst)))))) /\ (((((exists ff_h_pvs_transport_prefixfirstpositive. ff_h_pvs_transport_prefixfirstpositive + S (dst_positive_transport_prefixfirst) = S ((S (dst_index_transport_prefix)) * dst_positive_scale_transport_prefixfirst)) /\ exists ff_q_pvs_transport_prefixfirstpositive. dst_positive_code_transport_prefixfirst = ff_q_pvs_transport_prefixfirstpositive * S ((S (dst_index_transport_prefix)) * dst_positive_scale_transport_prefixfirst) + (dst_positive_transport_prefixfirst))) /\ (((((exists ff_h_pvs_transport_prefixfirstnegative. ff_h_pvs_transport_prefixfirstnegative + S (dst_negative_transport_prefixfirst) = S ((S (dst_index_transport_prefix)) * dst_negative_scale_transport_prefixfirst)) /\ exists ff_q_pvs_transport_prefixfirstnegative. dst_negative_code_transport_prefixfirst = ff_q_pvs_transport_prefixfirstnegative * S ((S (dst_index_transport_prefix)) * dst_negative_scale_transport_prefixfirst) + (dst_negative_transport_prefixfirst))) /\ (exists ge_balance_positive_transport_prefixfirstvalue ge_balance_negative_transport_prefixfirstvalue. (((((dst_first_transport_prefix) = 2 * (ge_balance_positive_transport_prefixfirstvalue) /\ (ge_balance_negative_transport_prefixfirstvalue) = 0) \/ exists ge_signed_half_transport_prefixfirstvaluedecode. (((dst_first_transport_prefix) = 2 * ge_signed_half_transport_prefixfirstvaluedecode + 1 /\ (ge_balance_positive_transport_prefixfirstvalue) = 0) /\ (ge_balance_negative_transport_prefixfirstvalue) = S ge_signed_half_transport_prefixfirstvaluedecode))) /\ ((dst_positive_transport_prefixfirst) + ge_balance_negative_transport_prefixfirstvalue = (dst_negative_transport_prefixfirst) + ge_balance_positive_transport_prefixfirstvalue))))))))) -> (exists dst_positive_code_transport_prefixsecond dst_positive_scale_transport_prefixsecond dst_negative_code_transport_prefixsecond dst_negative_scale_transport_prefixsecond dst_positive_transport_prefixsecond dst_negative_transport_prefixsecond. (((G) = (((((dst_positive_code_transport_prefixsecond) + (dst_positive_scale_transport_prefixsecond)) * S ((dst_positive_code_transport_prefixsecond) + (dst_positive_scale_transport_prefixsecond)) + ((dst_positive_scale_transport_prefixsecond) + (dst_positive_scale_transport_prefixsecond))) + (((dst_negative_code_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)) * S ((dst_negative_code_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)) + ((dst_negative_scale_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)))) * S ((((dst_positive_code_transport_prefixsecond) + (dst_positive_scale_transport_prefixsecond)) * S ((dst_positive_code_transport_prefixsecond) + (dst_positive_scale_transport_prefixsecond)) + ((dst_positive_scale_transport_prefixsecond) + (dst_positive_scale_transport_prefixsecond))) + (((dst_negative_code_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)) * S ((dst_negative_code_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)) + ((dst_negative_scale_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)))) + ((((dst_negative_code_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)) * S ((dst_negative_code_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)) + ((dst_negative_scale_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond))) + (((dst_negative_code_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)) * S ((dst_negative_code_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)) + ((dst_negative_scale_transport_prefixsecond) + (dst_negative_scale_transport_prefixsecond)))))) /\ (((((exists ff_h_pvs_transport_prefixsecondpositive. ff_h_pvs_transport_prefixsecondpositive + S (dst_positive_transport_prefixsecond) = S ((S (dst_index_transport_prefix)) * dst_positive_scale_transport_prefixsecond)) /\ exists ff_q_pvs_transport_prefixsecondpositive. dst_positive_code_transport_prefixsecond = ff_q_pvs_transport_prefixsecondpositive * S ((S (dst_index_transport_prefix)) * dst_positive_scale_transport_prefixsecond) + (dst_positive_transport_prefixsecond))) /\ (((((exists ff_h_pvs_transport_prefixsecondnegative. ff_h_pvs_transport_prefixsecondnegative + S (dst_negative_transport_prefixsecond) = S ((S (dst_index_transport_prefix)) * dst_negative_scale_transport_prefixsecond)) /\ exists ff_q_pvs_transport_prefixsecondnegative. dst_negative_code_transport_prefixsecond = ff_q_pvs_transport_prefixsecondnegative * S ((S (dst_index_transport_prefix)) * dst_negative_scale_transport_prefixsecond) + (dst_negative_transport_prefixsecond))) /\ (exists ge_balance_positive_transport_prefixsecondvalue ge_balance_negative_transport_prefixsecondvalue. (((((dst_second_transport_prefix) = 2 * (ge_balance_positive_transport_prefixsecondvalue) /\ (ge_balance_negative_transport_prefixsecondvalue) = 0) \/ exists ge_signed_half_transport_prefixsecondvaluedecode. (((dst_second_transport_prefix) = 2 * ge_signed_half_transport_prefixsecondvaluedecode + 1 /\ (ge_balance_positive_transport_prefixsecondvalue) = 0) /\ (ge_balance_negative_transport_prefixsecondvalue) = S ge_signed_half_transport_prefixsecondvaluedecode))) /\ ((dst_positive_transport_prefixsecond) + ge_balance_negative_transport_prefixsecondvalue = (dst_negative_transport_prefixsecond) + ge_balance_positive_transport_prefixsecondvalue))))))))) -> dst_first_transport_prefix = dst_second_transport_prefix) -> (exists pvs_le_gap_transport_domain. pvs_le_gap_transport_domain + (i) = (N)) -> (exists pvs_gap_transport_index. pvs_gap_transport_index + S (i) = (l)) -> (exists dst_positive_code_transport_source dst_positive_scale_transport_source dst_negative_code_transport_source dst_negative_scale_transport_source dst_positive_transport_source dst_negative_transport_source. (((F) = (((((dst_positive_code_transport_source) + (dst_positive_scale_transport_source)) * S ((dst_positive_code_transport_source) + (dst_positive_scale_transport_source)) + ((dst_positive_scale_transport_source) + (dst_positive_scale_transport_source))) + (((dst_negative_code_transport_source) + (dst_negative_scale_transport_source)) * S ((dst_negative_code_transport_source) + (dst_negative_scale_transport_source)) + ((dst_negative_scale_transport_source) + (dst_negative_scale_transport_source)))) * S ((((dst_positive_code_transport_source) + (dst_positive_scale_transport_source)) * S ((dst_positive_code_transport_source) + (dst_positive_scale_transport_source)) + ((dst_positive_scale_transport_source) + (dst_positive_scale_transport_source))) + (((dst_negative_code_transport_source) + (dst_negative_scale_transport_source)) * S ((dst_negative_code_transport_source) + (dst_negative_scale_transport_source)) + ((dst_negative_scale_transport_source) + (dst_negative_scale_transport_source)))) + ((((dst_negative_code_transport_source) + (dst_negative_scale_transport_source)) * S ((dst_negative_code_transport_source) + (dst_negative_scale_transport_source)) + ((dst_negative_scale_transport_source) + (dst_negative_scale_transport_source))) + (((dst_negative_code_transport_source) + (dst_negative_scale_transport_source)) * S ((dst_negative_code_transport_source) + (dst_negative_scale_transport_source)) + ((dst_negative_scale_transport_source) + (dst_negative_scale_transport_source)))))) /\ (((((exists ff_h_pvs_transport_sourcepositive. ff_h_pvs_transport_sourcepositive + S (dst_positive_transport_source) = S ((S (i)) * dst_positive_scale_transport_source)) /\ exists ff_q_pvs_transport_sourcepositive. dst_positive_code_transport_source = ff_q_pvs_transport_sourcepositive * S ((S (i)) * dst_positive_scale_transport_source) + (dst_positive_transport_source))) /\ (((((exists ff_h_pvs_transport_sourcenegative. ff_h_pvs_transport_sourcenegative + S (dst_negative_transport_source) = S ((S (i)) * dst_negative_scale_transport_source)) /\ exists ff_q_pvs_transport_sourcenegative. dst_negative_code_transport_source = ff_q_pvs_transport_sourcenegative * S ((S (i)) * dst_negative_scale_transport_source) + (dst_negative_transport_source))) /\ (exists ge_balance_positive_transport_sourcevalue ge_balance_negative_transport_sourcevalue. (((((z) = 2 * (ge_balance_positive_transport_sourcevalue) /\ (ge_balance_negative_transport_sourcevalue) = 0) \/ exists ge_signed_half_transport_sourcevaluedecode. (((z) = 2 * ge_signed_half_transport_sourcevaluedecode + 1 /\ (ge_balance_positive_transport_sourcevalue) = 0) /\ (ge_balance_negative_transport_sourcevalue) = S ge_signed_half_transport_sourcevaluedecode))) /\ ((dst_positive_transport_source) + ge_balance_negative_transport_sourcevalue = (dst_negative_transport_source) + ge_balance_positive_transport_sourcevalue))))))))) -> (exists dst_positive_code_transport_target dst_positive_scale_transport_target dst_negative_code_transport_target dst_negative_scale_transport_target dst_positive_transport_target dst_negative_transport_target. (((G) = (((((dst_positive_code_transport_target) + (dst_positive_scale_transport_target)) * S ((dst_positive_code_transport_target) + (dst_positive_scale_transport_target)) + ((dst_positive_scale_transport_target) + (dst_positive_scale_transport_target))) + (((dst_negative_code_transport_target) + (dst_negative_scale_transport_target)) * S ((dst_negative_code_transport_target) + (dst_negative_scale_transport_target)) + ((dst_negative_scale_transport_target) + (dst_negative_scale_transport_target)))) * S ((((dst_positive_code_transport_target) + (dst_positive_scale_transport_target)) * S ((dst_positive_code_transport_target) + (dst_positive_scale_transport_target)) + ((dst_positive_scale_transport_target) + (dst_positive_scale_transport_target))) + (((dst_negative_code_transport_target) + (dst_negative_scale_transport_target)) * S ((dst_negative_code_transport_target) + (dst_negative_scale_transport_target)) + ((dst_negative_scale_transport_target) + (dst_negative_scale_transport_target)))) + ((((dst_negative_code_transport_target) + (dst_negative_scale_transport_target)) * S ((dst_negative_code_transport_target) + (dst_negative_scale_transport_target)) + ((dst_negative_scale_transport_target) + (dst_negative_scale_transport_target))) + (((dst_negative_code_transport_target) + (dst_negative_scale_transport_target)) * S ((dst_negative_code_transport_target) + (dst_negative_scale_transport_target)) + ((dst_negative_scale_transport_target) + (dst_negative_scale_transport_target)))))) /\ (((((exists ff_h_pvs_transport_targetpositive. ff_h_pvs_transport_targetpositive + S (dst_positive_transport_target) = S ((S (i)) * dst_positive_scale_transport_target)) /\ exists ff_q_pvs_transport_targetpositive. dst_positive_code_transport_target = ff_q_pvs_transport_targetpositive * S ((S (i)) * dst_positive_scale_transport_target) + (dst_positive_transport_target))) /\ (((((exists ff_h_pvs_transport_targetnegative. ff_h_pvs_transport_targetnegative + S (dst_negative_transport_target) = S ((S (i)) * dst_negative_scale_transport_target)) /\ exists ff_q_pvs_transport_targetnegative. dst_negative_code_transport_target = ff_q_pvs_transport_targetnegative * S ((S (i)) * dst_negative_scale_transport_target) + (dst_negative_transport_target))) /\ (exists ge_balance_positive_transport_targetvalue ge_balance_negative_transport_targetvalue. (((((z) = 2 * (ge_balance_positive_transport_targetvalue) /\ (ge_balance_negative_transport_targetvalue) = 0) \/ exists ge_signed_half_transport_targetvaluedecode. (((z) = 2 * ge_signed_half_transport_targetvaluedecode + 1 /\ (ge_balance_positive_transport_targetvalue) = 0) /\ (ge_balance_negative_transport_targetvalue) = S ge_signed_half_transport_targetvaluedecode))) /\ ((dst_positive_transport_target) + ge_balance_negative_transport_targetvalue = (dst_negative_transport_target) + ge_balance_positive_transport_targetvalue)))))))))

arithmetic_signed_table_extend_at · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F l z. (exists dst_positive_code_extend_input dst_positive_scale_extend_input dst_negative_code_extend_input dst_negative_scale_extend_input. (((F) = (((((dst_positive_code_extend_input) + (dst_positive_scale_extend_input)) * S ((dst_positive_code_extend_input) + (dst_positive_scale_extend_input)) + ((dst_positive_scale_extend_input) + (dst_positive_scale_extend_input))) + (((dst_negative_code_extend_input) + (dst_negative_scale_extend_input)) * S ((dst_negative_code_extend_input) + (dst_negative_scale_extend_input)) + ((dst_negative_scale_extend_input) + (dst_negative_scale_extend_input)))) * S ((((dst_positive_code_extend_input) + (dst_positive_scale_extend_input)) * S ((dst_positive_code_extend_input) + (dst_positive_scale_extend_input)) + ((dst_positive_scale_extend_input) + (dst_positive_scale_extend_input))) + (((dst_negative_code_extend_input) + (dst_negative_scale_extend_input)) * S ((dst_negative_code_extend_input) + (dst_negative_scale_extend_input)) + ((dst_negative_scale_extend_input) + (dst_negative_scale_extend_input)))) + ((((dst_negative_code_extend_input) + (dst_negative_scale_extend_input)) * S ((dst_negative_code_extend_input) + (dst_negative_scale_extend_input)) + ((dst_negative_scale_extend_input) + (dst_negative_scale_extend_input))) + (((dst_negative_code_extend_input) + (dst_negative_scale_extend_input)) * S ((dst_negative_code_extend_input) + (dst_negative_scale_extend_input)) + ((dst_negative_scale_extend_input) + (dst_negative_scale_extend_input)))))) /\ (forall dst_index_extend_input. (exists pvs_le_gap_extend_inputdomain. pvs_le_gap_extend_inputdomain + (dst_index_extend_input) = (N)) -> exists dst_positive_extend_input dst_negative_extend_input dst_value_extend_input. ((((exists ff_h_pvs_extend_inputentrypositive. ff_h_pvs_extend_inputentrypositive + S (dst_positive_extend_input) = S ((S (dst_index_extend_input)) * dst_positive_scale_extend_input)) /\ exists ff_q_pvs_extend_inputentrypositive. dst_positive_code_extend_input = ff_q_pvs_extend_inputentrypositive * S ((S (dst_index_extend_input)) * dst_positive_scale_extend_input) + (dst_positive_extend_input))) /\ (((((exists ff_h_pvs_extend_inputentrynegative. ff_h_pvs_extend_inputentrynegative + S (dst_negative_extend_input) = S ((S (dst_index_extend_input)) * dst_negative_scale_extend_input)) /\ exists ff_q_pvs_extend_inputentrynegative. dst_negative_code_extend_input = ff_q_pvs_extend_inputentrynegative * S ((S (dst_index_extend_input)) * dst_negative_scale_extend_input) + (dst_negative_extend_input))) /\ (exists ge_balance_positive_extend_inputentryvalue ge_balance_negative_extend_inputentryvalue. (((((dst_value_extend_input) = 2 * (ge_balance_positive_extend_inputentryvalue) /\ (ge_balance_negative_extend_inputentryvalue) = 0) \/ exists ge_signed_half_extend_inputentryvaluedecode. (((dst_value_extend_input) = 2 * ge_signed_half_extend_inputentryvaluedecode + 1 /\ (ge_balance_positive_extend_inputentryvalue) = 0) /\ (ge_balance_negative_extend_inputentryvalue) = S ge_signed_half_extend_inputentryvaluedecode))) /\ ((dst_positive_extend_input) + ge_balance_negative_extend_inputentryvalue = (dst_negative_extend_input) + ge_balance_positive_extend_inputentryvalue))))))))) -> exists G. (((exists dst_positive_code_extend_outputtable dst_positive_scale_extend_outputtable dst_negative_code_extend_outputtable dst_negative_scale_extend_outputtable. (((G) = (((((dst_positive_code_extend_outputtable) + (dst_positive_scale_extend_outputtable)) * S ((dst_positive_code_extend_outputtable) + (dst_positive_scale_extend_outputtable)) + ((dst_positive_scale_extend_outputtable) + (dst_positive_scale_extend_outputtable))) + (((dst_negative_code_extend_outputtable) + (dst_negative_scale_extend_outputtable)) * S ((dst_negative_code_extend_outputtable) + (dst_negative_scale_extend_outputtable)) + ((dst_negative_scale_extend_outputtable) + (dst_negative_scale_extend_outputtable)))) * S ((((dst_positive_code_extend_outputtable) + (dst_positive_scale_extend_outputtable)) * S ((dst_positive_code_extend_outputtable) + (dst_positive_scale_extend_outputtable)) + ((dst_positive_scale_extend_outputtable) + (dst_positive_scale_extend_outputtable))) + (((dst_negative_code_extend_outputtable) + (dst_negative_scale_extend_outputtable)) * S ((dst_negative_code_extend_outputtable) + (dst_negative_scale_extend_outputtable)) + ((dst_negative_scale_extend_outputtable) + (dst_negative_scale_extend_outputtable)))) + ((((dst_negative_code_extend_outputtable) + (dst_negative_scale_extend_outputtable)) * S ((dst_negative_code_extend_outputtable) + (dst_negative_scale_extend_outputtable)) + ((dst_negative_scale_extend_outputtable) + (dst_negative_scale_extend_outputtable))) + (((dst_negative_code_extend_outputtable) + (dst_negative_scale_extend_outputtable)) * S ((dst_negative_code_extend_outputtable) + (dst_negative_scale_extend_outputtable)) + ((dst_negative_scale_extend_outputtable) + (dst_negative_scale_extend_outputtable)))))) /\ (forall dst_index_extend_outputtable. (exists pvs_le_gap_extend_outputtabledomain. pvs_le_gap_extend_outputtabledomain + (dst_index_extend_outputtable) = (l)) -> exists dst_positive_extend_outputtable dst_negative_extend_outputtable dst_value_extend_outputtable. ((((exists ff_h_pvs_extend_outputtableentrypositive. ff_h_pvs_extend_outputtableentrypositive + S (dst_positive_extend_outputtable) = S ((S (dst_index_extend_outputtable)) * dst_positive_scale_extend_outputtable)) /\ exists ff_q_pvs_extend_outputtableentrypositive. dst_positive_code_extend_outputtable = ff_q_pvs_extend_outputtableentrypositive * S ((S (dst_index_extend_outputtable)) * dst_positive_scale_extend_outputtable) + (dst_positive_extend_outputtable))) /\ (((((exists ff_h_pvs_extend_outputtableentrynegative. ff_h_pvs_extend_outputtableentrynegative + S (dst_negative_extend_outputtable) = S ((S (dst_index_extend_outputtable)) * dst_negative_scale_extend_outputtable)) /\ exists ff_q_pvs_extend_outputtableentrynegative. dst_negative_code_extend_outputtable = ff_q_pvs_extend_outputtableentrynegative * S ((S (dst_index_extend_outputtable)) * dst_negative_scale_extend_outputtable) + (dst_negative_extend_outputtable))) /\ (exists ge_balance_positive_extend_outputtableentryvalue ge_balance_negative_extend_outputtableentryvalue. (((((dst_value_extend_outputtable) = 2 * (ge_balance_positive_extend_outputtableentryvalue) /\ (ge_balance_negative_extend_outputtableentryvalue) = 0) \/ exists ge_signed_half_extend_outputtableentryvaluedecode. (((dst_value_extend_outputtable) = 2 * ge_signed_half_extend_outputtableentryvaluedecode + 1 /\ (ge_balance_positive_extend_outputtableentryvalue) = 0) /\ (ge_balance_negative_extend_outputtableentryvalue) = S ge_signed_half_extend_outputtableentryvaluedecode))) /\ ((dst_positive_extend_outputtable) + ge_balance_negative_extend_outputtableentryvalue = (dst_negative_extend_outputtable) + ge_balance_positive_extend_outputtableentryvalue))))))))) /\ (((forall dst_index_extend_outputprefix dst_first_extend_outputprefix dst_second_extend_outputprefix. (exists pvs_gap_extend_outputprefixbound. pvs_gap_extend_outputprefixbound + S (dst_index_extend_outputprefix) = (l)) -> (exists dst_positive_code_extend_outputprefixfirst dst_positive_scale_extend_outputprefixfirst dst_negative_code_extend_outputprefixfirst dst_negative_scale_extend_outputprefixfirst dst_positive_extend_outputprefixfirst dst_negative_extend_outputprefixfirst. (((F) = (((((dst_positive_code_extend_outputprefixfirst) + (dst_positive_scale_extend_outputprefixfirst)) * S ((dst_positive_code_extend_outputprefixfirst) + (dst_positive_scale_extend_outputprefixfirst)) + ((dst_positive_scale_extend_outputprefixfirst) + (dst_positive_scale_extend_outputprefixfirst))) + (((dst_negative_code_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)) * S ((dst_negative_code_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)) + ((dst_negative_scale_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)))) * S ((((dst_positive_code_extend_outputprefixfirst) + (dst_positive_scale_extend_outputprefixfirst)) * S ((dst_positive_code_extend_outputprefixfirst) + (dst_positive_scale_extend_outputprefixfirst)) + ((dst_positive_scale_extend_outputprefixfirst) + (dst_positive_scale_extend_outputprefixfirst))) + (((dst_negative_code_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)) * S ((dst_negative_code_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)) + ((dst_negative_scale_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)))) + ((((dst_negative_code_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)) * S ((dst_negative_code_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)) + ((dst_negative_scale_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst))) + (((dst_negative_code_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)) * S ((dst_negative_code_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)) + ((dst_negative_scale_extend_outputprefixfirst) + (dst_negative_scale_extend_outputprefixfirst)))))) /\ (((((exists ff_h_pvs_extend_outputprefixfirstpositive. ff_h_pvs_extend_outputprefixfirstpositive + S (dst_positive_extend_outputprefixfirst) = S ((S (dst_index_extend_outputprefix)) * dst_positive_scale_extend_outputprefixfirst)) /\ exists ff_q_pvs_extend_outputprefixfirstpositive. dst_positive_code_extend_outputprefixfirst = ff_q_pvs_extend_outputprefixfirstpositive * S ((S (dst_index_extend_outputprefix)) * dst_positive_scale_extend_outputprefixfirst) + (dst_positive_extend_outputprefixfirst))) /\ (((((exists ff_h_pvs_extend_outputprefixfirstnegative. ff_h_pvs_extend_outputprefixfirstnegative + S (dst_negative_extend_outputprefixfirst) = S ((S (dst_index_extend_outputprefix)) * dst_negative_scale_extend_outputprefixfirst)) /\ exists ff_q_pvs_extend_outputprefixfirstnegative. dst_negative_code_extend_outputprefixfirst = ff_q_pvs_extend_outputprefixfirstnegative * S ((S (dst_index_extend_outputprefix)) * dst_negative_scale_extend_outputprefixfirst) + (dst_negative_extend_outputprefixfirst))) /\ (exists ge_balance_positive_extend_outputprefixfirstvalue ge_balance_negative_extend_outputprefixfirstvalue. (((((dst_first_extend_outputprefix) = 2 * (ge_balance_positive_extend_outputprefixfirstvalue) /\ (ge_balance_negative_extend_outputprefixfirstvalue) = 0) \/ exists ge_signed_half_extend_outputprefixfirstvaluedecode. (((dst_first_extend_outputprefix) = 2 * ge_signed_half_extend_outputprefixfirstvaluedecode + 1 /\ (ge_balance_positive_extend_outputprefixfirstvalue) = 0) /\ (ge_balance_negative_extend_outputprefixfirstvalue) = S ge_signed_half_extend_outputprefixfirstvaluedecode))) /\ ((dst_positive_extend_outputprefixfirst) + ge_balance_negative_extend_outputprefixfirstvalue = (dst_negative_extend_outputprefixfirst) + ge_balance_positive_extend_outputprefixfirstvalue))))))))) -> (exists dst_positive_code_extend_outputprefixsecond dst_positive_scale_extend_outputprefixsecond dst_negative_code_extend_outputprefixsecond dst_negative_scale_extend_outputprefixsecond dst_positive_extend_outputprefixsecond dst_negative_extend_outputprefixsecond. (((G) = (((((dst_positive_code_extend_outputprefixsecond) + (dst_positive_scale_extend_outputprefixsecond)) * S ((dst_positive_code_extend_outputprefixsecond) + (dst_positive_scale_extend_outputprefixsecond)) + ((dst_positive_scale_extend_outputprefixsecond) + (dst_positive_scale_extend_outputprefixsecond))) + (((dst_negative_code_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)) * S ((dst_negative_code_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)) + ((dst_negative_scale_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)))) * S ((((dst_positive_code_extend_outputprefixsecond) + (dst_positive_scale_extend_outputprefixsecond)) * S ((dst_positive_code_extend_outputprefixsecond) + (dst_positive_scale_extend_outputprefixsecond)) + ((dst_positive_scale_extend_outputprefixsecond) + (dst_positive_scale_extend_outputprefixsecond))) + (((dst_negative_code_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)) * S ((dst_negative_code_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)) + ((dst_negative_scale_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)))) + ((((dst_negative_code_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)) * S ((dst_negative_code_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)) + ((dst_negative_scale_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond))) + (((dst_negative_code_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)) * S ((dst_negative_code_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)) + ((dst_negative_scale_extend_outputprefixsecond) + (dst_negative_scale_extend_outputprefixsecond)))))) /\ (((((exists ff_h_pvs_extend_outputprefixsecondpositive. ff_h_pvs_extend_outputprefixsecondpositive + S (dst_positive_extend_outputprefixsecond) = S ((S (dst_index_extend_outputprefix)) * dst_positive_scale_extend_outputprefixsecond)) /\ exists ff_q_pvs_extend_outputprefixsecondpositive. dst_positive_code_extend_outputprefixsecond = ff_q_pvs_extend_outputprefixsecondpositive * S ((S (dst_index_extend_outputprefix)) * dst_positive_scale_extend_outputprefixsecond) + (dst_positive_extend_outputprefixsecond))) /\ (((((exists ff_h_pvs_extend_outputprefixsecondnegative. ff_h_pvs_extend_outputprefixsecondnegative + S (dst_negative_extend_outputprefixsecond) = S ((S (dst_index_extend_outputprefix)) * dst_negative_scale_extend_outputprefixsecond)) /\ exists ff_q_pvs_extend_outputprefixsecondnegative. dst_negative_code_extend_outputprefixsecond = ff_q_pvs_extend_outputprefixsecondnegative * S ((S (dst_index_extend_outputprefix)) * dst_negative_scale_extend_outputprefixsecond) + (dst_negative_extend_outputprefixsecond))) /\ (exists ge_balance_positive_extend_outputprefixsecondvalue ge_balance_negative_extend_outputprefixsecondvalue. (((((dst_second_extend_outputprefix) = 2 * (ge_balance_positive_extend_outputprefixsecondvalue) /\ (ge_balance_negative_extend_outputprefixsecondvalue) = 0) \/ exists ge_signed_half_extend_outputprefixsecondvaluedecode. (((dst_second_extend_outputprefix) = 2 * ge_signed_half_extend_outputprefixsecondvaluedecode + 1 /\ (ge_balance_positive_extend_outputprefixsecondvalue) = 0) /\ (ge_balance_negative_extend_outputprefixsecondvalue) = S ge_signed_half_extend_outputprefixsecondvaluedecode))) /\ ((dst_positive_extend_outputprefixsecond) + ge_balance_negative_extend_outputprefixsecondvalue = (dst_negative_extend_outputprefixsecond) + ge_balance_positive_extend_outputprefixsecondvalue))))))))) -> dst_first_extend_outputprefix = dst_second_extend_outputprefix) /\ (exists dst_positive_code_extend_outputlast dst_positive_scale_extend_outputlast dst_negative_code_extend_outputlast dst_negative_scale_extend_outputlast dst_positive_extend_outputlast dst_negative_extend_outputlast. (((G) = (((((dst_positive_code_extend_outputlast) + (dst_positive_scale_extend_outputlast)) * S ((dst_positive_code_extend_outputlast) + (dst_positive_scale_extend_outputlast)) + ((dst_positive_scale_extend_outputlast) + (dst_positive_scale_extend_outputlast))) + (((dst_negative_code_extend_outputlast) + (dst_negative_scale_extend_outputlast)) * S ((dst_negative_code_extend_outputlast) + (dst_negative_scale_extend_outputlast)) + ((dst_negative_scale_extend_outputlast) + (dst_negative_scale_extend_outputlast)))) * S ((((dst_positive_code_extend_outputlast) + (dst_positive_scale_extend_outputlast)) * S ((dst_positive_code_extend_outputlast) + (dst_positive_scale_extend_outputlast)) + ((dst_positive_scale_extend_outputlast) + (dst_positive_scale_extend_outputlast))) + (((dst_negative_code_extend_outputlast) + (dst_negative_scale_extend_outputlast)) * S ((dst_negative_code_extend_outputlast) + (dst_negative_scale_extend_outputlast)) + ((dst_negative_scale_extend_outputlast) + (dst_negative_scale_extend_outputlast)))) + ((((dst_negative_code_extend_outputlast) + (dst_negative_scale_extend_outputlast)) * S ((dst_negative_code_extend_outputlast) + (dst_negative_scale_extend_outputlast)) + ((dst_negative_scale_extend_outputlast) + (dst_negative_scale_extend_outputlast))) + (((dst_negative_code_extend_outputlast) + (dst_negative_scale_extend_outputlast)) * S ((dst_negative_code_extend_outputlast) + (dst_negative_scale_extend_outputlast)) + ((dst_negative_scale_extend_outputlast) + (dst_negative_scale_extend_outputlast)))))) /\ (((((exists ff_h_pvs_extend_outputlastpositive. ff_h_pvs_extend_outputlastpositive + S (dst_positive_extend_outputlast) = S ((S (l)) * dst_positive_scale_extend_outputlast)) /\ exists ff_q_pvs_extend_outputlastpositive. dst_positive_code_extend_outputlast = ff_q_pvs_extend_outputlastpositive * S ((S (l)) * dst_positive_scale_extend_outputlast) + (dst_positive_extend_outputlast))) /\ (((((exists ff_h_pvs_extend_outputlastnegative. ff_h_pvs_extend_outputlastnegative + S (dst_negative_extend_outputlast) = S ((S (l)) * dst_negative_scale_extend_outputlast)) /\ exists ff_q_pvs_extend_outputlastnegative. dst_negative_code_extend_outputlast = ff_q_pvs_extend_outputlastnegative * S ((S (l)) * dst_negative_scale_extend_outputlast) + (dst_negative_extend_outputlast))) /\ (exists ge_balance_positive_extend_outputlastvalue ge_balance_negative_extend_outputlastvalue. (((((z) = 2 * (ge_balance_positive_extend_outputlastvalue) /\ (ge_balance_negative_extend_outputlastvalue) = 0) \/ exists ge_signed_half_extend_outputlastvaluedecode. (((z) = 2 * ge_signed_half_extend_outputlastvaluedecode + 1 /\ (ge_balance_positive_extend_outputlastvalue) = 0) /\ (ge_balance_negative_extend_outputlastvalue) = S ge_signed_half_extend_outputlastvaluedecode))) /\ ((dst_positive_extend_outputlast) + ge_balance_negative_extend_outputlastvalue = (dst_negative_extend_outputlast) + ge_balance_positive_extend_outputlastvalue)))))))))))))

divisor_signed_sum_empty_value · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F z. (exists dst_positive_code_empty_sum dst_positive_scale_empty_sum dst_negative_code_empty_sum dst_negative_scale_empty_sum dst_positive_sum_empty_sum dst_negative_sum_empty_sum. (((F) = (((((dst_positive_code_empty_sum) + (dst_positive_scale_empty_sum)) * S ((dst_positive_code_empty_sum) + (dst_positive_scale_empty_sum)) + ((dst_positive_scale_empty_sum) + (dst_positive_scale_empty_sum))) + (((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) * S ((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) + ((dst_negative_scale_empty_sum) + (dst_negative_scale_empty_sum)))) * S ((((dst_positive_code_empty_sum) + (dst_positive_scale_empty_sum)) * S ((dst_positive_code_empty_sum) + (dst_positive_scale_empty_sum)) + ((dst_positive_scale_empty_sum) + (dst_positive_scale_empty_sum))) + (((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) * S ((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) + ((dst_negative_scale_empty_sum) + (dst_negative_scale_empty_sum)))) + ((((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) * S ((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) + ((dst_negative_scale_empty_sum) + (dst_negative_scale_empty_sum))) + (((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) * S ((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) + ((dst_negative_scale_empty_sum) + (dst_negative_scale_empty_sum)))))) /\ (((exists fs_u_dst_empty_sumpositive fs_v_dst_empty_sumpositive. ((((exists fs_h_dst_empty_sumpositive_body_start. fs_h_dst_empty_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_empty_sumpositive)) /\ exists fs_q_dst_empty_sumpositive_body_start. fs_u_dst_empty_sumpositive = fs_q_dst_empty_sumpositive_body_start * S ((S (0)) * fs_v_dst_empty_sumpositive) + (0))) /\ ((((exists fs_h_dst_empty_sumpositive_body_terminal. fs_h_dst_empty_sumpositive_body_terminal + S (dst_positive_sum_empty_sum) = S ((S (0)) * fs_v_dst_empty_sumpositive)) /\ exists fs_q_dst_empty_sumpositive_body_terminal. fs_u_dst_empty_sumpositive = fs_q_dst_empty_sumpositive_body_terminal * S ((S (0)) * fs_v_dst_empty_sumpositive) + (dst_positive_sum_empty_sum))) /\ forall fs_i_dst_empty_sumpositive_body_steps. (exists fs_lt_dst_empty_sumpositive_body_steps_bound. fs_lt_dst_empty_sumpositive_body_steps_bound + S fs_i_dst_empty_sumpositive_body_steps = 0) -> exists fs_a_dst_empty_sumpositive_body_steps fs_r_dst_empty_sumpositive_body_steps fs_s_dst_empty_sumpositive_body_steps. ((((exists fs_h_dst_empty_sumpositive_body_steps_summand. fs_h_dst_empty_sumpositive_body_steps_summand + S (fs_a_dst_empty_sumpositive_body_steps) = S ((S (fs_i_dst_empty_sumpositive_body_steps)) * dst_positive_scale_empty_sum)) /\ exists fs_q_dst_empty_sumpositive_body_steps_summand. dst_positive_code_empty_sum = fs_q_dst_empty_sumpositive_body_steps_summand * S ((S (fs_i_dst_empty_sumpositive_body_steps)) * dst_positive_scale_empty_sum) + (fs_a_dst_empty_sumpositive_body_steps))) /\ ((((exists fs_h_dst_empty_sumpositive_body_steps_partial. fs_h_dst_empty_sumpositive_body_steps_partial + S (fs_r_dst_empty_sumpositive_body_steps) = S ((S (fs_i_dst_empty_sumpositive_body_steps)) * fs_v_dst_empty_sumpositive)) /\ exists fs_q_dst_empty_sumpositive_body_steps_partial. fs_u_dst_empty_sumpositive = fs_q_dst_empty_sumpositive_body_steps_partial * S ((S (fs_i_dst_empty_sumpositive_body_steps)) * fs_v_dst_empty_sumpositive) + (fs_r_dst_empty_sumpositive_body_steps))) /\ ((((exists fs_h_dst_empty_sumpositive_body_steps_successor. fs_h_dst_empty_sumpositive_body_steps_successor + S (fs_s_dst_empty_sumpositive_body_steps) = S ((S (S fs_i_dst_empty_sumpositive_body_steps)) * fs_v_dst_empty_sumpositive)) /\ exists fs_q_dst_empty_sumpositive_body_steps_successor. fs_u_dst_empty_sumpositive = fs_q_dst_empty_sumpositive_body_steps_successor * S ((S (S fs_i_dst_empty_sumpositive_body_steps)) * fs_v_dst_empty_sumpositive) + (fs_s_dst_empty_sumpositive_body_steps))) /\ fs_s_dst_empty_sumpositive_body_steps = fs_r_dst_empty_sumpositive_body_steps + fs_a_dst_empty_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_empty_sumnegative fs_v_dst_empty_sumnegative. ((((exists fs_h_dst_empty_sumnegative_body_start. fs_h_dst_empty_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_empty_sumnegative)) /\ exists fs_q_dst_empty_sumnegative_body_start. fs_u_dst_empty_sumnegative = fs_q_dst_empty_sumnegative_body_start * S ((S (0)) * fs_v_dst_empty_sumnegative) + (0))) /\ ((((exists fs_h_dst_empty_sumnegative_body_terminal. fs_h_dst_empty_sumnegative_body_terminal + S (dst_negative_sum_empty_sum) = S ((S (0)) * fs_v_dst_empty_sumnegative)) /\ exists fs_q_dst_empty_sumnegative_body_terminal. fs_u_dst_empty_sumnegative = fs_q_dst_empty_sumnegative_body_terminal * S ((S (0)) * fs_v_dst_empty_sumnegative) + (dst_negative_sum_empty_sum))) /\ forall fs_i_dst_empty_sumnegative_body_steps. (exists fs_lt_dst_empty_sumnegative_body_steps_bound. fs_lt_dst_empty_sumnegative_body_steps_bound + S fs_i_dst_empty_sumnegative_body_steps = 0) -> exists fs_a_dst_empty_sumnegative_body_steps fs_r_dst_empty_sumnegative_body_steps fs_s_dst_empty_sumnegative_body_steps. ((((exists fs_h_dst_empty_sumnegative_body_steps_summand. fs_h_dst_empty_sumnegative_body_steps_summand + S (fs_a_dst_empty_sumnegative_body_steps) = S ((S (fs_i_dst_empty_sumnegative_body_steps)) * dst_negative_scale_empty_sum)) /\ exists fs_q_dst_empty_sumnegative_body_steps_summand. dst_negative_code_empty_sum = fs_q_dst_empty_sumnegative_body_steps_summand * S ((S (fs_i_dst_empty_sumnegative_body_steps)) * dst_negative_scale_empty_sum) + (fs_a_dst_empty_sumnegative_body_steps))) /\ ((((exists fs_h_dst_empty_sumnegative_body_steps_partial. fs_h_dst_empty_sumnegative_body_steps_partial + S (fs_r_dst_empty_sumnegative_body_steps) = S ((S (fs_i_dst_empty_sumnegative_body_steps)) * fs_v_dst_empty_sumnegative)) /\ exists fs_q_dst_empty_sumnegative_body_steps_partial. fs_u_dst_empty_sumnegative = fs_q_dst_empty_sumnegative_body_steps_partial * S ((S (fs_i_dst_empty_sumnegative_body_steps)) * fs_v_dst_empty_sumnegative) + (fs_r_dst_empty_sumnegative_body_steps))) /\ ((((exists fs_h_dst_empty_sumnegative_body_steps_successor. fs_h_dst_empty_sumnegative_body_steps_successor + S (fs_s_dst_empty_sumnegative_body_steps) = S ((S (S fs_i_dst_empty_sumnegative_body_steps)) * fs_v_dst_empty_sumnegative)) /\ exists fs_q_dst_empty_sumnegative_body_steps_successor. fs_u_dst_empty_sumnegative = fs_q_dst_empty_sumnegative_body_steps_successor * S ((S (S fs_i_dst_empty_sumnegative_body_steps)) * fs_v_dst_empty_sumnegative) + (fs_s_dst_empty_sumnegative_body_steps))) /\ fs_s_dst_empty_sumnegative_body_steps = fs_r_dst_empty_sumnegative_body_steps + fs_a_dst_empty_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_empty_sumresult ge_balance_negative_empty_sumresult. (((((z) = 2 * (ge_balance_positive_empty_sumresult) /\ (ge_balance_negative_empty_sumresult) = 0) \/ exists ge_signed_half_empty_sumresultdecode. (((z) = 2 * ge_signed_half_empty_sumresultdecode + 1 /\ (ge_balance_positive_empty_sumresult) = 0) /\ (ge_balance_negative_empty_sumresult) = S ge_signed_half_empty_sumresultdecode))) /\ ((dst_positive_sum_empty_sum) + ge_balance_negative_empty_sumresult = (dst_negative_sum_empty_sum) + ge_balance_positive_empty_sumresult))))))))) -> z = 0

divisor_signed_sum_extensional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F G l a b. (forall dst_index_sum_ext_entries dst_first_sum_ext_entries dst_second_sum_ext_entries. (exists pvs_gap_sum_ext_entriesbound. pvs_gap_sum_ext_entriesbound + S (dst_index_sum_ext_entries) = (l)) -> (exists dst_positive_code_sum_ext_entriesfirst dst_positive_scale_sum_ext_entriesfirst dst_negative_code_sum_ext_entriesfirst dst_negative_scale_sum_ext_entriesfirst dst_positive_sum_ext_entriesfirst dst_negative_sum_ext_entriesfirst. (((F) = (((((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) * S ((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) + ((dst_positive_scale_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst))) + (((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)))) * S ((((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) * S ((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) + ((dst_positive_scale_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst))) + (((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)))) + ((((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst))) + (((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)))))) /\ (((((exists ff_h_pvs_sum_ext_entriesfirstpositive. ff_h_pvs_sum_ext_entriesfirstpositive + S (dst_positive_sum_ext_entriesfirst) = S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriesfirst)) /\ exists ff_q_pvs_sum_ext_entriesfirstpositive. dst_positive_code_sum_ext_entriesfirst = ff_q_pvs_sum_ext_entriesfirstpositive * S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriesfirst) + (dst_positive_sum_ext_entriesfirst))) /\ (((((exists ff_h_pvs_sum_ext_entriesfirstnegative. ff_h_pvs_sum_ext_entriesfirstnegative + S (dst_negative_sum_ext_entriesfirst) = S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriesfirst)) /\ exists ff_q_pvs_sum_ext_entriesfirstnegative. dst_negative_code_sum_ext_entriesfirst = ff_q_pvs_sum_ext_entriesfirstnegative * S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_sum_ext_entriesfirst))) /\ (exists ge_balance_positive_sum_ext_entriesfirstvalue ge_balance_negative_sum_ext_entriesfirstvalue. (((((dst_first_sum_ext_entries) = 2 * (ge_balance_positive_sum_ext_entriesfirstvalue) /\ (ge_balance_negative_sum_ext_entriesfirstvalue) = 0) \/ exists ge_signed_half_sum_ext_entriesfirstvaluedecode. (((dst_first_sum_ext_entries) = 2 * ge_signed_half_sum_ext_entriesfirstvaluedecode + 1 /\ (ge_balance_positive_sum_ext_entriesfirstvalue) = 0) /\ (ge_balance_negative_sum_ext_entriesfirstvalue) = S ge_signed_half_sum_ext_entriesfirstvaluedecode))) /\ ((dst_positive_sum_ext_entriesfirst) + ge_balance_negative_sum_ext_entriesfirstvalue = (dst_negative_sum_ext_entriesfirst) + ge_balance_positive_sum_ext_entriesfirstvalue))))))))) -> (exists dst_positive_code_sum_ext_entriessecond dst_positive_scale_sum_ext_entriessecond dst_negative_code_sum_ext_entriessecond dst_negative_scale_sum_ext_entriessecond dst_positive_sum_ext_entriessecond dst_negative_sum_ext_entriessecond. (((G) = (((((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) * S ((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) + ((dst_positive_scale_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond))) + (((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)))) * S ((((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) * S ((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) + ((dst_positive_scale_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond))) + (((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)))) + ((((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond))) + (((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)))))) /\ (((((exists ff_h_pvs_sum_ext_entriessecondpositive. ff_h_pvs_sum_ext_entriessecondpositive + S (dst_positive_sum_ext_entriessecond) = S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriessecond)) /\ exists ff_q_pvs_sum_ext_entriessecondpositive. dst_positive_code_sum_ext_entriessecond = ff_q_pvs_sum_ext_entriessecondpositive * S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriessecond) + (dst_positive_sum_ext_entriessecond))) /\ (((((exists ff_h_pvs_sum_ext_entriessecondnegative. ff_h_pvs_sum_ext_entriessecondnegative + S (dst_negative_sum_ext_entriessecond) = S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriessecond)) /\ exists ff_q_pvs_sum_ext_entriessecondnegative. dst_negative_code_sum_ext_entriessecond = ff_q_pvs_sum_ext_entriessecondnegative * S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriessecond) + (dst_negative_sum_ext_entriessecond))) /\ (exists ge_balance_positive_sum_ext_entriessecondvalue ge_balance_negative_sum_ext_entriessecondvalue. (((((dst_second_sum_ext_entries) = 2 * (ge_balance_positive_sum_ext_entriessecondvalue) /\ (ge_balance_negative_sum_ext_entriessecondvalue) = 0) \/ exists ge_signed_half_sum_ext_entriessecondvaluedecode. (((dst_second_sum_ext_entries) = 2 * ge_signed_half_sum_ext_entriessecondvaluedecode + 1 /\ (ge_balance_positive_sum_ext_entriessecondvalue) = 0) /\ (ge_balance_negative_sum_ext_entriessecondvalue) = S ge_signed_half_sum_ext_entriessecondvaluedecode))) /\ ((dst_positive_sum_ext_entriessecond) + ge_balance_negative_sum_ext_entriessecondvalue = (dst_negative_sum_ext_entriessecond) + ge_balance_positive_sum_ext_entriessecondvalue))))))))) -> dst_first_sum_ext_entries = dst_second_sum_ext_entries) -> (exists dst_positive_code_sum_ext_first dst_positive_scale_sum_ext_first dst_negative_code_sum_ext_first dst_negative_scale_sum_ext_first dst_positive_sum_sum_ext_first dst_negative_sum_sum_ext_first. (((F) = (((((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) * S ((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) + ((dst_positive_scale_sum_ext_first) + (dst_positive_scale_sum_ext_first))) + (((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first)))) * S ((((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) * S ((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) + ((dst_positive_scale_sum_ext_first) + (dst_positive_scale_sum_ext_first))) + (((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first)))) + ((((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first))) + (((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first)))))) /\ (((exists fs_u_dst_sum_ext_firstpositive fs_v_dst_sum_ext_firstpositive. ((((exists fs_h_dst_sum_ext_firstpositive_body_start. fs_h_dst_sum_ext_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_start. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_start * S ((S (0)) * fs_v_dst_sum_ext_firstpositive) + (0))) /\ ((((exists fs_h_dst_sum_ext_firstpositive_body_terminal. fs_h_dst_sum_ext_firstpositive_body_terminal + S (dst_positive_sum_sum_ext_first) = S ((S (l)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_terminal. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_firstpositive) + (dst_positive_sum_sum_ext_first))) /\ forall fs_i_dst_sum_ext_firstpositive_body_steps. (exists fs_lt_dst_sum_ext_firstpositive_body_steps_bound. fs_lt_dst_sum_ext_firstpositive_body_steps_bound + S fs_i_dst_sum_ext_firstpositive_body_steps = l) -> exists fs_a_dst_sum_ext_firstpositive_body_steps fs_r_dst_sum_ext_firstpositive_body_steps fs_s_dst_sum_ext_firstpositive_body_steps. ((((exists fs_h_dst_sum_ext_firstpositive_body_steps_summand. fs_h_dst_sum_ext_firstpositive_body_steps_summand + S (fs_a_dst_sum_ext_firstpositive_body_steps) = S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * dst_positive_scale_sum_ext_first)) /\ exists fs_q_dst_sum_ext_firstpositive_body_steps_summand. dst_positive_code_sum_ext_first = fs_q_dst_sum_ext_firstpositive_body_steps_summand * S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * dst_positive_scale_sum_ext_first) + (fs_a_dst_sum_ext_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstpositive_body_steps_partial. fs_h_dst_sum_ext_firstpositive_body_steps_partial + S (fs_r_dst_sum_ext_firstpositive_body_steps) = S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_steps_partial. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_steps_partial * S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive) + (fs_r_dst_sum_ext_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstpositive_body_steps_successor. fs_h_dst_sum_ext_firstpositive_body_steps_successor + S (fs_s_dst_sum_ext_firstpositive_body_steps) = S ((S (S fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_steps_successor. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_steps_successor * S ((S (S fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive) + (fs_s_dst_sum_ext_firstpositive_body_steps))) /\ fs_s_dst_sum_ext_firstpositive_body_steps = fs_r_dst_sum_ext_firstpositive_body_steps + fs_a_dst_sum_ext_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_ext_firstnegative fs_v_dst_sum_ext_firstnegative. ((((exists fs_h_dst_sum_ext_firstnegative_body_start. fs_h_dst_sum_ext_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_start. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_start * S ((S (0)) * fs_v_dst_sum_ext_firstnegative) + (0))) /\ ((((exists fs_h_dst_sum_ext_firstnegative_body_terminal. fs_h_dst_sum_ext_firstnegative_body_terminal + S (dst_negative_sum_sum_ext_first) = S ((S (l)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_terminal. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_firstnegative) + (dst_negative_sum_sum_ext_first))) /\ forall fs_i_dst_sum_ext_firstnegative_body_steps. (exists fs_lt_dst_sum_ext_firstnegative_body_steps_bound. fs_lt_dst_sum_ext_firstnegative_body_steps_bound + S fs_i_dst_sum_ext_firstnegative_body_steps = l) -> exists fs_a_dst_sum_ext_firstnegative_body_steps fs_r_dst_sum_ext_firstnegative_body_steps fs_s_dst_sum_ext_firstnegative_body_steps. ((((exists fs_h_dst_sum_ext_firstnegative_body_steps_summand. fs_h_dst_sum_ext_firstnegative_body_steps_summand + S (fs_a_dst_sum_ext_firstnegative_body_steps) = S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * dst_negative_scale_sum_ext_first)) /\ exists fs_q_dst_sum_ext_firstnegative_body_steps_summand. dst_negative_code_sum_ext_first = fs_q_dst_sum_ext_firstnegative_body_steps_summand * S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * dst_negative_scale_sum_ext_first) + (fs_a_dst_sum_ext_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstnegative_body_steps_partial. fs_h_dst_sum_ext_firstnegative_body_steps_partial + S (fs_r_dst_sum_ext_firstnegative_body_steps) = S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_steps_partial. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_steps_partial * S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative) + (fs_r_dst_sum_ext_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstnegative_body_steps_successor. fs_h_dst_sum_ext_firstnegative_body_steps_successor + S (fs_s_dst_sum_ext_firstnegative_body_steps) = S ((S (S fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_steps_successor. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_steps_successor * S ((S (S fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative) + (fs_s_dst_sum_ext_firstnegative_body_steps))) /\ fs_s_dst_sum_ext_firstnegative_body_steps = fs_r_dst_sum_ext_firstnegative_body_steps + fs_a_dst_sum_ext_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_ext_firstresult ge_balance_negative_sum_ext_firstresult. (((((a) = 2 * (ge_balance_positive_sum_ext_firstresult) /\ (ge_balance_negative_sum_ext_firstresult) = 0) \/ exists ge_signed_half_sum_ext_firstresultdecode. (((a) = 2 * ge_signed_half_sum_ext_firstresultdecode + 1 /\ (ge_balance_positive_sum_ext_firstresult) = 0) /\ (ge_balance_negative_sum_ext_firstresult) = S ge_signed_half_sum_ext_firstresultdecode))) /\ ((dst_positive_sum_sum_ext_first) + ge_balance_negative_sum_ext_firstresult = (dst_negative_sum_sum_ext_first) + ge_balance_positive_sum_ext_firstresult))))))))) -> (exists dst_positive_code_sum_ext_second dst_positive_scale_sum_ext_second dst_negative_code_sum_ext_second dst_negative_scale_sum_ext_second dst_positive_sum_sum_ext_second dst_negative_sum_sum_ext_second. (((G) = (((((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) * S ((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) + ((dst_positive_scale_sum_ext_second) + (dst_positive_scale_sum_ext_second))) + (((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second)))) * S ((((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) * S ((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) + ((dst_positive_scale_sum_ext_second) + (dst_positive_scale_sum_ext_second))) + (((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second)))) + ((((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second))) + (((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second)))))) /\ (((exists fs_u_dst_sum_ext_secondpositive fs_v_dst_sum_ext_secondpositive. ((((exists fs_h_dst_sum_ext_secondpositive_body_start. fs_h_dst_sum_ext_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_start. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_start * S ((S (0)) * fs_v_dst_sum_ext_secondpositive) + (0))) /\ ((((exists fs_h_dst_sum_ext_secondpositive_body_terminal. fs_h_dst_sum_ext_secondpositive_body_terminal + S (dst_positive_sum_sum_ext_second) = S ((S (l)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_terminal. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_secondpositive) + (dst_positive_sum_sum_ext_second))) /\ forall fs_i_dst_sum_ext_secondpositive_body_steps. (exists fs_lt_dst_sum_ext_secondpositive_body_steps_bound. fs_lt_dst_sum_ext_secondpositive_body_steps_bound + S fs_i_dst_sum_ext_secondpositive_body_steps = l) -> exists fs_a_dst_sum_ext_secondpositive_body_steps fs_r_dst_sum_ext_secondpositive_body_steps fs_s_dst_sum_ext_secondpositive_body_steps. ((((exists fs_h_dst_sum_ext_secondpositive_body_steps_summand. fs_h_dst_sum_ext_secondpositive_body_steps_summand + S (fs_a_dst_sum_ext_secondpositive_body_steps) = S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * dst_positive_scale_sum_ext_second)) /\ exists fs_q_dst_sum_ext_secondpositive_body_steps_summand. dst_positive_code_sum_ext_second = fs_q_dst_sum_ext_secondpositive_body_steps_summand * S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * dst_positive_scale_sum_ext_second) + (fs_a_dst_sum_ext_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondpositive_body_steps_partial. fs_h_dst_sum_ext_secondpositive_body_steps_partial + S (fs_r_dst_sum_ext_secondpositive_body_steps) = S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_steps_partial. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_steps_partial * S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive) + (fs_r_dst_sum_ext_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondpositive_body_steps_successor. fs_h_dst_sum_ext_secondpositive_body_steps_successor + S (fs_s_dst_sum_ext_secondpositive_body_steps) = S ((S (S fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_steps_successor. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_steps_successor * S ((S (S fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive) + (fs_s_dst_sum_ext_secondpositive_body_steps))) /\ fs_s_dst_sum_ext_secondpositive_body_steps = fs_r_dst_sum_ext_secondpositive_body_steps + fs_a_dst_sum_ext_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_ext_secondnegative fs_v_dst_sum_ext_secondnegative. ((((exists fs_h_dst_sum_ext_secondnegative_body_start. fs_h_dst_sum_ext_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_start. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_start * S ((S (0)) * fs_v_dst_sum_ext_secondnegative) + (0))) /\ ((((exists fs_h_dst_sum_ext_secondnegative_body_terminal. fs_h_dst_sum_ext_secondnegative_body_terminal + S (dst_negative_sum_sum_ext_second) = S ((S (l)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_terminal. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_secondnegative) + (dst_negative_sum_sum_ext_second))) /\ forall fs_i_dst_sum_ext_secondnegative_body_steps. (exists fs_lt_dst_sum_ext_secondnegative_body_steps_bound. fs_lt_dst_sum_ext_secondnegative_body_steps_bound + S fs_i_dst_sum_ext_secondnegative_body_steps = l) -> exists fs_a_dst_sum_ext_secondnegative_body_steps fs_r_dst_sum_ext_secondnegative_body_steps fs_s_dst_sum_ext_secondnegative_body_steps. ((((exists fs_h_dst_sum_ext_secondnegative_body_steps_summand. fs_h_dst_sum_ext_secondnegative_body_steps_summand + S (fs_a_dst_sum_ext_secondnegative_body_steps) = S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * dst_negative_scale_sum_ext_second)) /\ exists fs_q_dst_sum_ext_secondnegative_body_steps_summand. dst_negative_code_sum_ext_second = fs_q_dst_sum_ext_secondnegative_body_steps_summand * S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * dst_negative_scale_sum_ext_second) + (fs_a_dst_sum_ext_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondnegative_body_steps_partial. fs_h_dst_sum_ext_secondnegative_body_steps_partial + S (fs_r_dst_sum_ext_secondnegative_body_steps) = S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_steps_partial. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_steps_partial * S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative) + (fs_r_dst_sum_ext_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondnegative_body_steps_successor. fs_h_dst_sum_ext_secondnegative_body_steps_successor + S (fs_s_dst_sum_ext_secondnegative_body_steps) = S ((S (S fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_steps_successor. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_steps_successor * S ((S (S fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative) + (fs_s_dst_sum_ext_secondnegative_body_steps))) /\ fs_s_dst_sum_ext_secondnegative_body_steps = fs_r_dst_sum_ext_secondnegative_body_steps + fs_a_dst_sum_ext_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_ext_secondresult ge_balance_negative_sum_ext_secondresult. (((((b) = 2 * (ge_balance_positive_sum_ext_secondresult) /\ (ge_balance_negative_sum_ext_secondresult) = 0) \/ exists ge_signed_half_sum_ext_secondresultdecode. (((b) = 2 * ge_signed_half_sum_ext_secondresultdecode + 1 /\ (ge_balance_positive_sum_ext_secondresult) = 0) /\ (ge_balance_negative_sum_ext_secondresult) = S ge_signed_half_sum_ext_secondresultdecode))) /\ ((dst_positive_sum_sum_ext_second) + ge_balance_negative_sum_ext_secondresult = (dst_negative_sum_sum_ext_second) + ge_balance_positive_sum_ext_secondresult))))))))) -> a = b

divisor_signed_sum_successor_decompose · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F l z. (exists dst_positive_code_decomp_sum dst_positive_scale_decomp_sum dst_negative_code_decomp_sum dst_negative_scale_decomp_sum dst_positive_sum_decomp_sum dst_negative_sum_decomp_sum. (((F) = (((((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) * S ((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) + ((dst_positive_scale_decomp_sum) + (dst_positive_scale_decomp_sum))) + (((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum)))) * S ((((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) * S ((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) + ((dst_positive_scale_decomp_sum) + (dst_positive_scale_decomp_sum))) + (((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum)))) + ((((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum))) + (((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum)))))) /\ (((exists fs_u_dst_decomp_sumpositive fs_v_dst_decomp_sumpositive. ((((exists fs_h_dst_decomp_sumpositive_body_start. fs_h_dst_decomp_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_start. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_start * S ((S (0)) * fs_v_dst_decomp_sumpositive) + (0))) /\ ((((exists fs_h_dst_decomp_sumpositive_body_terminal. fs_h_dst_decomp_sumpositive_body_terminal + S (dst_positive_sum_decomp_sum) = S ((S (S l)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_terminal. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_terminal * S ((S (S l)) * fs_v_dst_decomp_sumpositive) + (dst_positive_sum_decomp_sum))) /\ forall fs_i_dst_decomp_sumpositive_body_steps. (exists fs_lt_dst_decomp_sumpositive_body_steps_bound. fs_lt_dst_decomp_sumpositive_body_steps_bound + S fs_i_dst_decomp_sumpositive_body_steps = S l) -> exists fs_a_dst_decomp_sumpositive_body_steps fs_r_dst_decomp_sumpositive_body_steps fs_s_dst_decomp_sumpositive_body_steps. ((((exists fs_h_dst_decomp_sumpositive_body_steps_summand. fs_h_dst_decomp_sumpositive_body_steps_summand + S (fs_a_dst_decomp_sumpositive_body_steps) = S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * dst_positive_scale_decomp_sum)) /\ exists fs_q_dst_decomp_sumpositive_body_steps_summand. dst_positive_code_decomp_sum = fs_q_dst_decomp_sumpositive_body_steps_summand * S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * dst_positive_scale_decomp_sum) + (fs_a_dst_decomp_sumpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_sumpositive_body_steps_partial. fs_h_dst_decomp_sumpositive_body_steps_partial + S (fs_r_dst_decomp_sumpositive_body_steps) = S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_steps_partial. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_steps_partial * S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive) + (fs_r_dst_decomp_sumpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_sumpositive_body_steps_successor. fs_h_dst_decomp_sumpositive_body_steps_successor + S (fs_s_dst_decomp_sumpositive_body_steps) = S ((S (S fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_steps_successor. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_steps_successor * S ((S (S fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive) + (fs_s_dst_decomp_sumpositive_body_steps))) /\ fs_s_dst_decomp_sumpositive_body_steps = fs_r_dst_decomp_sumpositive_body_steps + fs_a_dst_decomp_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_decomp_sumnegative fs_v_dst_decomp_sumnegative. ((((exists fs_h_dst_decomp_sumnegative_body_start. fs_h_dst_decomp_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_start. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_start * S ((S (0)) * fs_v_dst_decomp_sumnegative) + (0))) /\ ((((exists fs_h_dst_decomp_sumnegative_body_terminal. fs_h_dst_decomp_sumnegative_body_terminal + S (dst_negative_sum_decomp_sum) = S ((S (S l)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_terminal. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_terminal * S ((S (S l)) * fs_v_dst_decomp_sumnegative) + (dst_negative_sum_decomp_sum))) /\ forall fs_i_dst_decomp_sumnegative_body_steps. (exists fs_lt_dst_decomp_sumnegative_body_steps_bound. fs_lt_dst_decomp_sumnegative_body_steps_bound + S fs_i_dst_decomp_sumnegative_body_steps = S l) -> exists fs_a_dst_decomp_sumnegative_body_steps fs_r_dst_decomp_sumnegative_body_steps fs_s_dst_decomp_sumnegative_body_steps. ((((exists fs_h_dst_decomp_sumnegative_body_steps_summand. fs_h_dst_decomp_sumnegative_body_steps_summand + S (fs_a_dst_decomp_sumnegative_body_steps) = S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * dst_negative_scale_decomp_sum)) /\ exists fs_q_dst_decomp_sumnegative_body_steps_summand. dst_negative_code_decomp_sum = fs_q_dst_decomp_sumnegative_body_steps_summand * S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * dst_negative_scale_decomp_sum) + (fs_a_dst_decomp_sumnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_sumnegative_body_steps_partial. fs_h_dst_decomp_sumnegative_body_steps_partial + S (fs_r_dst_decomp_sumnegative_body_steps) = S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_steps_partial. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_steps_partial * S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative) + (fs_r_dst_decomp_sumnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_sumnegative_body_steps_successor. fs_h_dst_decomp_sumnegative_body_steps_successor + S (fs_s_dst_decomp_sumnegative_body_steps) = S ((S (S fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_steps_successor. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_steps_successor * S ((S (S fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative) + (fs_s_dst_decomp_sumnegative_body_steps))) /\ fs_s_dst_decomp_sumnegative_body_steps = fs_r_dst_decomp_sumnegative_body_steps + fs_a_dst_decomp_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_decomp_sumresult ge_balance_negative_decomp_sumresult. (((((z) = 2 * (ge_balance_positive_decomp_sumresult) /\ (ge_balance_negative_decomp_sumresult) = 0) \/ exists ge_signed_half_decomp_sumresultdecode. (((z) = 2 * ge_signed_half_decomp_sumresultdecode + 1 /\ (ge_balance_positive_decomp_sumresult) = 0) /\ (ge_balance_negative_decomp_sumresult) = S ge_signed_half_decomp_sumresultdecode))) /\ ((dst_positive_sum_decomp_sum) + ge_balance_negative_decomp_sumresult = (dst_negative_sum_decomp_sum) + ge_balance_positive_decomp_sumresult))))))))) -> exists a b. ((exists dst_positive_code_decomp_prefix dst_positive_scale_decomp_prefix dst_negative_code_decomp_prefix dst_negative_scale_decomp_prefix dst_positive_sum_decomp_prefix dst_negative_sum_decomp_prefix. (((F) = (((((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) * S ((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) + ((dst_positive_scale_decomp_prefix) + (dst_positive_scale_decomp_prefix))) + (((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix)))) * S ((((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) * S ((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) + ((dst_positive_scale_decomp_prefix) + (dst_positive_scale_decomp_prefix))) + (((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix)))) + ((((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix))) + (((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix)))))) /\ (((exists fs_u_dst_decomp_prefixpositive fs_v_dst_decomp_prefixpositive. ((((exists fs_h_dst_decomp_prefixpositive_body_start. fs_h_dst_decomp_prefixpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_start. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_start * S ((S (0)) * fs_v_dst_decomp_prefixpositive) + (0))) /\ ((((exists fs_h_dst_decomp_prefixpositive_body_terminal. fs_h_dst_decomp_prefixpositive_body_terminal + S (dst_positive_sum_decomp_prefix) = S ((S (l)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_terminal. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_terminal * S ((S (l)) * fs_v_dst_decomp_prefixpositive) + (dst_positive_sum_decomp_prefix))) /\ forall fs_i_dst_decomp_prefixpositive_body_steps. (exists fs_lt_dst_decomp_prefixpositive_body_steps_bound. fs_lt_dst_decomp_prefixpositive_body_steps_bound + S fs_i_dst_decomp_prefixpositive_body_steps = l) -> exists fs_a_dst_decomp_prefixpositive_body_steps fs_r_dst_decomp_prefixpositive_body_steps fs_s_dst_decomp_prefixpositive_body_steps. ((((exists fs_h_dst_decomp_prefixpositive_body_steps_summand. fs_h_dst_decomp_prefixpositive_body_steps_summand + S (fs_a_dst_decomp_prefixpositive_body_steps) = S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * dst_positive_scale_decomp_prefix)) /\ exists fs_q_dst_decomp_prefixpositive_body_steps_summand. dst_positive_code_decomp_prefix = fs_q_dst_decomp_prefixpositive_body_steps_summand * S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * dst_positive_scale_decomp_prefix) + (fs_a_dst_decomp_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixpositive_body_steps_partial. fs_h_dst_decomp_prefixpositive_body_steps_partial + S (fs_r_dst_decomp_prefixpositive_body_steps) = S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_steps_partial. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_steps_partial * S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive) + (fs_r_dst_decomp_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixpositive_body_steps_successor. fs_h_dst_decomp_prefixpositive_body_steps_successor + S (fs_s_dst_decomp_prefixpositive_body_steps) = S ((S (S fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_steps_successor. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_steps_successor * S ((S (S fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive) + (fs_s_dst_decomp_prefixpositive_body_steps))) /\ fs_s_dst_decomp_prefixpositive_body_steps = fs_r_dst_decomp_prefixpositive_body_steps + fs_a_dst_decomp_prefixpositive_body_steps)))))) /\ (((exists fs_u_dst_decomp_prefixnegative fs_v_dst_decomp_prefixnegative. ((((exists fs_h_dst_decomp_prefixnegative_body_start. fs_h_dst_decomp_prefixnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_start. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_start * S ((S (0)) * fs_v_dst_decomp_prefixnegative) + (0))) /\ ((((exists fs_h_dst_decomp_prefixnegative_body_terminal. fs_h_dst_decomp_prefixnegative_body_terminal + S (dst_negative_sum_decomp_prefix) = S ((S (l)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_terminal. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_terminal * S ((S (l)) * fs_v_dst_decomp_prefixnegative) + (dst_negative_sum_decomp_prefix))) /\ forall fs_i_dst_decomp_prefixnegative_body_steps. (exists fs_lt_dst_decomp_prefixnegative_body_steps_bound. fs_lt_dst_decomp_prefixnegative_body_steps_bound + S fs_i_dst_decomp_prefixnegative_body_steps = l) -> exists fs_a_dst_decomp_prefixnegative_body_steps fs_r_dst_decomp_prefixnegative_body_steps fs_s_dst_decomp_prefixnegative_body_steps. ((((exists fs_h_dst_decomp_prefixnegative_body_steps_summand. fs_h_dst_decomp_prefixnegative_body_steps_summand + S (fs_a_dst_decomp_prefixnegative_body_steps) = S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * dst_negative_scale_decomp_prefix)) /\ exists fs_q_dst_decomp_prefixnegative_body_steps_summand. dst_negative_code_decomp_prefix = fs_q_dst_decomp_prefixnegative_body_steps_summand * S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * dst_negative_scale_decomp_prefix) + (fs_a_dst_decomp_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixnegative_body_steps_partial. fs_h_dst_decomp_prefixnegative_body_steps_partial + S (fs_r_dst_decomp_prefixnegative_body_steps) = S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_steps_partial. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_steps_partial * S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative) + (fs_r_dst_decomp_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixnegative_body_steps_successor. fs_h_dst_decomp_prefixnegative_body_steps_successor + S (fs_s_dst_decomp_prefixnegative_body_steps) = S ((S (S fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_steps_successor. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_steps_successor * S ((S (S fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative) + (fs_s_dst_decomp_prefixnegative_body_steps))) /\ fs_s_dst_decomp_prefixnegative_body_steps = fs_r_dst_decomp_prefixnegative_body_steps + fs_a_dst_decomp_prefixnegative_body_steps)))))) /\ (exists ge_balance_positive_decomp_prefixresult ge_balance_negative_decomp_prefixresult. (((((a) = 2 * (ge_balance_positive_decomp_prefixresult) /\ (ge_balance_negative_decomp_prefixresult) = 0) \/ exists ge_signed_half_decomp_prefixresultdecode. (((a) = 2 * ge_signed_half_decomp_prefixresultdecode + 1 /\ (ge_balance_positive_decomp_prefixresult) = 0) /\ (ge_balance_negative_decomp_prefixresult) = S ge_signed_half_decomp_prefixresultdecode))) /\ ((dst_positive_sum_decomp_prefix) + ge_balance_negative_decomp_prefixresult = (dst_negative_sum_decomp_prefix) + ge_balance_positive_decomp_prefixresult))))))))) /\ (((exists dst_positive_code_decomp_entry dst_positive_scale_decomp_entry dst_negative_code_decomp_entry dst_negative_scale_decomp_entry dst_positive_decomp_entry dst_negative_decomp_entry. (((F) = (((((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) * S ((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) + ((dst_positive_scale_decomp_entry) + (dst_positive_scale_decomp_entry))) + (((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry)))) * S ((((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) * S ((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) + ((dst_positive_scale_decomp_entry) + (dst_positive_scale_decomp_entry))) + (((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry)))) + ((((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry))) + (((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry)))))) /\ (((((exists ff_h_pvs_decomp_entrypositive. ff_h_pvs_decomp_entrypositive + S (dst_positive_decomp_entry) = S ((S (l)) * dst_positive_scale_decomp_entry)) /\ exists ff_q_pvs_decomp_entrypositive. dst_positive_code_decomp_entry = ff_q_pvs_decomp_entrypositive * S ((S (l)) * dst_positive_scale_decomp_entry) + (dst_positive_decomp_entry))) /\ (((((exists ff_h_pvs_decomp_entrynegative. ff_h_pvs_decomp_entrynegative + S (dst_negative_decomp_entry) = S ((S (l)) * dst_negative_scale_decomp_entry)) /\ exists ff_q_pvs_decomp_entrynegative. dst_negative_code_decomp_entry = ff_q_pvs_decomp_entrynegative * S ((S (l)) * dst_negative_scale_decomp_entry) + (dst_negative_decomp_entry))) /\ (exists ge_balance_positive_decomp_entryvalue ge_balance_negative_decomp_entryvalue. (((((b) = 2 * (ge_balance_positive_decomp_entryvalue) /\ (ge_balance_negative_decomp_entryvalue) = 0) \/ exists ge_signed_half_decomp_entryvaluedecode. (((b) = 2 * ge_signed_half_decomp_entryvaluedecode + 1 /\ (ge_balance_positive_decomp_entryvalue) = 0) /\ (ge_balance_negative_decomp_entryvalue) = S ge_signed_half_decomp_entryvaluedecode))) /\ ((dst_positive_decomp_entry) + ge_balance_negative_decomp_entryvalue = (dst_negative_decomp_entry) + ge_balance_positive_decomp_entryvalue))))))))) /\ (exists dsa_ap_decomp_add dsa_an_decomp_add dsa_bp_decomp_add dsa_bn_decomp_add dsa_cp_decomp_add dsa_cn_decomp_add. (((((a) = 2 * (dsa_ap_decomp_add) /\ (dsa_an_decomp_add) = 0) \/ exists ge_signed_half_decomp_addleft. (((a) = 2 * ge_signed_half_decomp_addleft + 1 /\ (dsa_ap_decomp_add) = 0) /\ (dsa_an_decomp_add) = S ge_signed_half_decomp_addleft))) /\ ((((((b) = 2 * (dsa_bp_decomp_add) /\ (dsa_bn_decomp_add) = 0) \/ exists ge_signed_half_decomp_addright. (((b) = 2 * ge_signed_half_decomp_addright + 1 /\ (dsa_bp_decomp_add) = 0) /\ (dsa_bn_decomp_add) = S ge_signed_half_decomp_addright))) /\ ((((((z) = 2 * (dsa_cp_decomp_add) /\ (dsa_cn_decomp_add) = 0) \/ exists ge_signed_half_decomp_addoutput. (((z) = 2 * ge_signed_half_decomp_addoutput + 1 /\ (dsa_cp_decomp_add) = 0) /\ (dsa_cn_decomp_add) = S ge_signed_half_decomp_addoutput))) /\ ((dsa_ap_decomp_add + dsa_bp_decomp_add) + dsa_cn_decomp_add = (dsa_an_decomp_add + dsa_bn_decomp_add) + dsa_cp_decomp_add))))))))))

divisor_signed_table_at_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F i a b. (exists dst_positive_code_functional_first dst_positive_scale_functional_first dst_negative_code_functional_first dst_negative_scale_functional_first dst_positive_functional_first dst_negative_functional_first. (((F) = (((((dst_positive_code_functional_first) + (dst_positive_scale_functional_first)) * S ((dst_positive_code_functional_first) + (dst_positive_scale_functional_first)) + ((dst_positive_scale_functional_first) + (dst_positive_scale_functional_first))) + (((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) * S ((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) + ((dst_negative_scale_functional_first) + (dst_negative_scale_functional_first)))) * S ((((dst_positive_code_functional_first) + (dst_positive_scale_functional_first)) * S ((dst_positive_code_functional_first) + (dst_positive_scale_functional_first)) + ((dst_positive_scale_functional_first) + (dst_positive_scale_functional_first))) + (((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) * S ((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) + ((dst_negative_scale_functional_first) + (dst_negative_scale_functional_first)))) + ((((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) * S ((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) + ((dst_negative_scale_functional_first) + (dst_negative_scale_functional_first))) + (((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) * S ((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) + ((dst_negative_scale_functional_first) + (dst_negative_scale_functional_first)))))) /\ (((((exists ff_h_pvs_functional_firstpositive. ff_h_pvs_functional_firstpositive + S (dst_positive_functional_first) = S ((S (i)) * dst_positive_scale_functional_first)) /\ exists ff_q_pvs_functional_firstpositive. dst_positive_code_functional_first = ff_q_pvs_functional_firstpositive * S ((S (i)) * dst_positive_scale_functional_first) + (dst_positive_functional_first))) /\ (((((exists ff_h_pvs_functional_firstnegative. ff_h_pvs_functional_firstnegative + S (dst_negative_functional_first) = S ((S (i)) * dst_negative_scale_functional_first)) /\ exists ff_q_pvs_functional_firstnegative. dst_negative_code_functional_first = ff_q_pvs_functional_firstnegative * S ((S (i)) * dst_negative_scale_functional_first) + (dst_negative_functional_first))) /\ (exists ge_balance_positive_functional_firstvalue ge_balance_negative_functional_firstvalue. (((((a) = 2 * (ge_balance_positive_functional_firstvalue) /\ (ge_balance_negative_functional_firstvalue) = 0) \/ exists ge_signed_half_functional_firstvaluedecode. (((a) = 2 * ge_signed_half_functional_firstvaluedecode + 1 /\ (ge_balance_positive_functional_firstvalue) = 0) /\ (ge_balance_negative_functional_firstvalue) = S ge_signed_half_functional_firstvaluedecode))) /\ ((dst_positive_functional_first) + ge_balance_negative_functional_firstvalue = (dst_negative_functional_first) + ge_balance_positive_functional_firstvalue))))))))) -> (exists dst_positive_code_functional_second dst_positive_scale_functional_second dst_negative_code_functional_second dst_negative_scale_functional_second dst_positive_functional_second dst_negative_functional_second. (((F) = (((((dst_positive_code_functional_second) + (dst_positive_scale_functional_second)) * S ((dst_positive_code_functional_second) + (dst_positive_scale_functional_second)) + ((dst_positive_scale_functional_second) + (dst_positive_scale_functional_second))) + (((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) * S ((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) + ((dst_negative_scale_functional_second) + (dst_negative_scale_functional_second)))) * S ((((dst_positive_code_functional_second) + (dst_positive_scale_functional_second)) * S ((dst_positive_code_functional_second) + (dst_positive_scale_functional_second)) + ((dst_positive_scale_functional_second) + (dst_positive_scale_functional_second))) + (((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) * S ((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) + ((dst_negative_scale_functional_second) + (dst_negative_scale_functional_second)))) + ((((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) * S ((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) + ((dst_negative_scale_functional_second) + (dst_negative_scale_functional_second))) + (((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) * S ((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) + ((dst_negative_scale_functional_second) + (dst_negative_scale_functional_second)))))) /\ (((((exists ff_h_pvs_functional_secondpositive. ff_h_pvs_functional_secondpositive + S (dst_positive_functional_second) = S ((S (i)) * dst_positive_scale_functional_second)) /\ exists ff_q_pvs_functional_secondpositive. dst_positive_code_functional_second = ff_q_pvs_functional_secondpositive * S ((S (i)) * dst_positive_scale_functional_second) + (dst_positive_functional_second))) /\ (((((exists ff_h_pvs_functional_secondnegative. ff_h_pvs_functional_secondnegative + S (dst_negative_functional_second) = S ((S (i)) * dst_negative_scale_functional_second)) /\ exists ff_q_pvs_functional_secondnegative. dst_negative_code_functional_second = ff_q_pvs_functional_secondnegative * S ((S (i)) * dst_negative_scale_functional_second) + (dst_negative_functional_second))) /\ (exists ge_balance_positive_functional_secondvalue ge_balance_negative_functional_secondvalue. (((((b) = 2 * (ge_balance_positive_functional_secondvalue) /\ (ge_balance_negative_functional_secondvalue) = 0) \/ exists ge_signed_half_functional_secondvaluedecode. (((b) = 2 * ge_signed_half_functional_secondvaluedecode + 1 /\ (ge_balance_positive_functional_secondvalue) = 0) /\ (ge_balance_negative_functional_secondvalue) = S ge_signed_half_functional_secondvaluedecode))) /\ ((dst_positive_functional_second) + ge_balance_negative_functional_secondvalue = (dst_negative_functional_second) + ge_balance_positive_functional_secondvalue))))))))) -> a = b

divisor_signed_table_components · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F. (exists dst_positive_code_extract_table dst_positive_scale_extract_table dst_negative_code_extract_table dst_negative_scale_extract_table. (((F) = (((((dst_positive_code_extract_table) + (dst_positive_scale_extract_table)) * S ((dst_positive_code_extract_table) + (dst_positive_scale_extract_table)) + ((dst_positive_scale_extract_table) + (dst_positive_scale_extract_table))) + (((dst_negative_code_extract_table) + (dst_negative_scale_extract_table)) * S ((dst_negative_code_extract_table) + (dst_negative_scale_extract_table)) + ((dst_negative_scale_extract_table) + (dst_negative_scale_extract_table)))) * S ((((dst_positive_code_extract_table) + (dst_positive_scale_extract_table)) * S ((dst_positive_code_extract_table) + (dst_positive_scale_extract_table)) + ((dst_positive_scale_extract_table) + (dst_positive_scale_extract_table))) + (((dst_negative_code_extract_table) + (dst_negative_scale_extract_table)) * S ((dst_negative_code_extract_table) + (dst_negative_scale_extract_table)) + ((dst_negative_scale_extract_table) + (dst_negative_scale_extract_table)))) + ((((dst_negative_code_extract_table) + (dst_negative_scale_extract_table)) * S ((dst_negative_code_extract_table) + (dst_negative_scale_extract_table)) + ((dst_negative_scale_extract_table) + (dst_negative_scale_extract_table))) + (((dst_negative_code_extract_table) + (dst_negative_scale_extract_table)) * S ((dst_negative_code_extract_table) + (dst_negative_scale_extract_table)) + ((dst_negative_scale_extract_table) + (dst_negative_scale_extract_table)))))) /\ (forall dst_index_extract_table. (exists pvs_le_gap_extract_tabledomain. pvs_le_gap_extract_tabledomain + (dst_index_extract_table) = (N)) -> exists dst_positive_extract_table dst_negative_extract_table dst_value_extract_table. ((((exists ff_h_pvs_extract_tableentrypositive. ff_h_pvs_extract_tableentrypositive + S (dst_positive_extract_table) = S ((S (dst_index_extract_table)) * dst_positive_scale_extract_table)) /\ exists ff_q_pvs_extract_tableentrypositive. dst_positive_code_extract_table = ff_q_pvs_extract_tableentrypositive * S ((S (dst_index_extract_table)) * dst_positive_scale_extract_table) + (dst_positive_extract_table))) /\ (((((exists ff_h_pvs_extract_tableentrynegative. ff_h_pvs_extract_tableentrynegative + S (dst_negative_extract_table) = S ((S (dst_index_extract_table)) * dst_negative_scale_extract_table)) /\ exists ff_q_pvs_extract_tableentrynegative. dst_negative_code_extract_table = ff_q_pvs_extract_tableentrynegative * S ((S (dst_index_extract_table)) * dst_negative_scale_extract_table) + (dst_negative_extract_table))) /\ (exists ge_balance_positive_extract_tableentryvalue ge_balance_negative_extract_tableentryvalue. (((((dst_value_extract_table) = 2 * (ge_balance_positive_extract_tableentryvalue) /\ (ge_balance_negative_extract_tableentryvalue) = 0) \/ exists ge_signed_half_extract_tableentryvaluedecode. (((dst_value_extract_table) = 2 * ge_signed_half_extract_tableentryvaluedecode + 1 /\ (ge_balance_positive_extract_tableentryvalue) = 0) /\ (ge_balance_negative_extract_tableentryvalue) = S ge_signed_half_extract_tableentryvaluedecode))) /\ ((dst_positive_extract_table) + ge_balance_negative_extract_tableentryvalue = (dst_negative_extract_table) + ge_balance_positive_extract_tableentryvalue))))))))) -> exists pb pc nb nc. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))))))

divisor_signed_table_from_components · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F pb pc nb nc. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> (exists dst_positive_code_constructor_table dst_positive_scale_constructor_table dst_negative_code_constructor_table dst_negative_scale_constructor_table. (((F) = (((((dst_positive_code_constructor_table) + (dst_positive_scale_constructor_table)) * S ((dst_positive_code_constructor_table) + (dst_positive_scale_constructor_table)) + ((dst_positive_scale_constructor_table) + (dst_positive_scale_constructor_table))) + (((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) * S ((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) + ((dst_negative_scale_constructor_table) + (dst_negative_scale_constructor_table)))) * S ((((dst_positive_code_constructor_table) + (dst_positive_scale_constructor_table)) * S ((dst_positive_code_constructor_table) + (dst_positive_scale_constructor_table)) + ((dst_positive_scale_constructor_table) + (dst_positive_scale_constructor_table))) + (((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) * S ((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) + ((dst_negative_scale_constructor_table) + (dst_negative_scale_constructor_table)))) + ((((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) * S ((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) + ((dst_negative_scale_constructor_table) + (dst_negative_scale_constructor_table))) + (((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) * S ((dst_negative_code_constructor_table) + (dst_negative_scale_constructor_table)) + ((dst_negative_scale_constructor_table) + (dst_negative_scale_constructor_table)))))) /\ (forall dst_index_constructor_table. (exists pvs_le_gap_constructor_tabledomain. pvs_le_gap_constructor_tabledomain + (dst_index_constructor_table) = (N)) -> exists dst_positive_constructor_table dst_negative_constructor_table dst_value_constructor_table. ((((exists ff_h_pvs_constructor_tableentrypositive. ff_h_pvs_constructor_tableentrypositive + S (dst_positive_constructor_table) = S ((S (dst_index_constructor_table)) * dst_positive_scale_constructor_table)) /\ exists ff_q_pvs_constructor_tableentrypositive. dst_positive_code_constructor_table = ff_q_pvs_constructor_tableentrypositive * S ((S (dst_index_constructor_table)) * dst_positive_scale_constructor_table) + (dst_positive_constructor_table))) /\ (((((exists ff_h_pvs_constructor_tableentrynegative. ff_h_pvs_constructor_tableentrynegative + S (dst_negative_constructor_table) = S ((S (dst_index_constructor_table)) * dst_negative_scale_constructor_table)) /\ exists ff_q_pvs_constructor_tableentrynegative. dst_negative_code_constructor_table = ff_q_pvs_constructor_tableentrynegative * S ((S (dst_index_constructor_table)) * dst_negative_scale_constructor_table) + (dst_negative_constructor_table))) /\ (exists ge_balance_positive_constructor_tableentryvalue ge_balance_negative_constructor_tableentryvalue. (((((dst_value_constructor_table) = 2 * (ge_balance_positive_constructor_tableentryvalue) /\ (ge_balance_negative_constructor_tableentryvalue) = 0) \/ exists ge_signed_half_constructor_tableentryvaluedecode. (((dst_value_constructor_table) = 2 * ge_signed_half_constructor_tableentryvaluedecode + 1 /\ (ge_balance_positive_constructor_tableentryvalue) = 0) /\ (ge_balance_negative_constructor_tableentryvalue) = S ge_signed_half_constructor_tableentryvaluedecode))) /\ ((dst_positive_constructor_table) + ge_balance_negative_constructor_tableentryvalue = (dst_negative_constructor_table) + ge_balance_positive_constructor_tableentryvalue)))))))))

divisor_signed_table_lookup · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F i. (exists dst_positive_code_lookup_table dst_positive_scale_lookup_table dst_negative_code_lookup_table dst_negative_scale_lookup_table. (((F) = (((((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) * S ((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) + ((dst_positive_scale_lookup_table) + (dst_positive_scale_lookup_table))) + (((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table)))) * S ((((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) * S ((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) + ((dst_positive_scale_lookup_table) + (dst_positive_scale_lookup_table))) + (((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table)))) + ((((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table))) + (((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table)))))) /\ (forall dst_index_lookup_table. (exists pvs_le_gap_lookup_tabledomain. pvs_le_gap_lookup_tabledomain + (dst_index_lookup_table) = (N)) -> exists dst_positive_lookup_table dst_negative_lookup_table dst_value_lookup_table. ((((exists ff_h_pvs_lookup_tableentrypositive. ff_h_pvs_lookup_tableentrypositive + S (dst_positive_lookup_table) = S ((S (dst_index_lookup_table)) * dst_positive_scale_lookup_table)) /\ exists ff_q_pvs_lookup_tableentrypositive. dst_positive_code_lookup_table = ff_q_pvs_lookup_tableentrypositive * S ((S (dst_index_lookup_table)) * dst_positive_scale_lookup_table) + (dst_positive_lookup_table))) /\ (((((exists ff_h_pvs_lookup_tableentrynegative. ff_h_pvs_lookup_tableentrynegative + S (dst_negative_lookup_table) = S ((S (dst_index_lookup_table)) * dst_negative_scale_lookup_table)) /\ exists ff_q_pvs_lookup_tableentrynegative. dst_negative_code_lookup_table = ff_q_pvs_lookup_tableentrynegative * S ((S (dst_index_lookup_table)) * dst_negative_scale_lookup_table) + (dst_negative_lookup_table))) /\ (exists ge_balance_positive_lookup_tableentryvalue ge_balance_negative_lookup_tableentryvalue. (((((dst_value_lookup_table) = 2 * (ge_balance_positive_lookup_tableentryvalue) /\ (ge_balance_negative_lookup_tableentryvalue) = 0) \/ exists ge_signed_half_lookup_tableentryvaluedecode. (((dst_value_lookup_table) = 2 * ge_signed_half_lookup_tableentryvaluedecode + 1 /\ (ge_balance_positive_lookup_tableentryvalue) = 0) /\ (ge_balance_negative_lookup_tableentryvalue) = S ge_signed_half_lookup_tableentryvaluedecode))) /\ ((dst_positive_lookup_table) + ge_balance_negative_lookup_tableentryvalue = (dst_negative_lookup_table) + ge_balance_positive_lookup_tableentryvalue))))))))) -> (exists pvs_le_gap_lookup_domain. pvs_le_gap_lookup_domain + (i) = (N)) -> exists z. (exists dst_positive_code_lookup_result dst_positive_scale_lookup_result dst_negative_code_lookup_result dst_negative_scale_lookup_result dst_positive_lookup_result dst_negative_lookup_result. (((F) = (((((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) * S ((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) + ((dst_positive_scale_lookup_result) + (dst_positive_scale_lookup_result))) + (((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result)))) * S ((((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) * S ((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) + ((dst_positive_scale_lookup_result) + (dst_positive_scale_lookup_result))) + (((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result)))) + ((((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result))) + (((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result)))))) /\ (((((exists ff_h_pvs_lookup_resultpositive. ff_h_pvs_lookup_resultpositive + S (dst_positive_lookup_result) = S ((S (i)) * dst_positive_scale_lookup_result)) /\ exists ff_q_pvs_lookup_resultpositive. dst_positive_code_lookup_result = ff_q_pvs_lookup_resultpositive * S ((S (i)) * dst_positive_scale_lookup_result) + (dst_positive_lookup_result))) /\ (((((exists ff_h_pvs_lookup_resultnegative. ff_h_pvs_lookup_resultnegative + S (dst_negative_lookup_result) = S ((S (i)) * dst_negative_scale_lookup_result)) /\ exists ff_q_pvs_lookup_resultnegative. dst_negative_code_lookup_result = ff_q_pvs_lookup_resultnegative * S ((S (i)) * dst_negative_scale_lookup_result) + (dst_negative_lookup_result))) /\ (exists ge_balance_positive_lookup_resultvalue ge_balance_negative_lookup_resultvalue. (((((z) = 2 * (ge_balance_positive_lookup_resultvalue) /\ (ge_balance_negative_lookup_resultvalue) = 0) \/ exists ge_signed_half_lookup_resultvaluedecode. (((z) = 2 * ge_signed_half_lookup_resultvaluedecode + 1 /\ (ge_balance_positive_lookup_resultvalue) = 0) /\ (ge_balance_negative_lookup_resultvalue) = S ge_signed_half_lookup_resultvaluedecode))) /\ ((dst_positive_lookup_result) + ge_balance_negative_lookup_resultvalue = (dst_negative_lookup_result) + ge_balance_positive_lookup_resultvalue)))))))))

finite_lt_succ_eq_or_lt · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n x. (exists h. h + S x = S n) -> x = n \/ exists h. h + S x = n
```
le_refl · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n <= n
```
le_succ · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + a = b) -> exists r. r + a = S b
```

signed_add_associative · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a b c ab bc abc. (exists sa_lp_assoc_ab sa_ln_assoc_ab sa_rp_assoc_ab sa_rn_assoc_ab sa_op_assoc_ab sa_on_assoc_ab. (((a = 2 * sa_lp_assoc_ab /\ sa_ln_assoc_ab = 0) \/ exists sd_half_assoc_ab_left. ((a = 2 * sd_half_assoc_ab_left + 1 /\ sa_lp_assoc_ab = 0) /\ sa_ln_assoc_ab = S sd_half_assoc_ab_left)) /\ (((b = 2 * sa_rp_assoc_ab /\ sa_rn_assoc_ab = 0) \/ exists sd_half_assoc_ab_right. ((b = 2 * sd_half_assoc_ab_right + 1 /\ sa_rp_assoc_ab = 0) /\ sa_rn_assoc_ab = S sd_half_assoc_ab_right)) /\ (((ab = 2 * sa_op_assoc_ab /\ sa_on_assoc_ab = 0) \/ exists sd_half_assoc_ab_output. ((ab = 2 * sd_half_assoc_ab_output + 1 /\ sa_op_assoc_ab = 0) /\ sa_on_assoc_ab = S sd_half_assoc_ab_output)) /\ (sa_lp_assoc_ab + sa_rp_assoc_ab) + sa_on_assoc_ab = (sa_ln_assoc_ab + sa_rn_assoc_ab) + sa_op_assoc_ab)))) -> (exists sa_lp_assoc_abc sa_ln_assoc_abc sa_rp_assoc_abc sa_rn_assoc_abc sa_op_assoc_abc sa_on_assoc_abc. (((ab = 2 * sa_lp_assoc_abc /\ sa_ln_assoc_abc = 0) \/ exists sd_half_assoc_abc_left. ((ab = 2 * sd_half_assoc_abc_left + 1 /\ sa_lp_assoc_abc = 0) /\ sa_ln_assoc_abc = S sd_half_assoc_abc_left)) /\ (((c = 2 * sa_rp_assoc_abc /\ sa_rn_assoc_abc = 0) \/ exists sd_half_assoc_abc_right. ((c = 2 * sd_half_assoc_abc_right + 1 /\ sa_rp_assoc_abc = 0) /\ sa_rn_assoc_abc = S sd_half_assoc_abc_right)) /\ (((abc = 2 * sa_op_assoc_abc /\ sa_on_assoc_abc = 0) \/ exists sd_half_assoc_abc_output. ((abc = 2 * sd_half_assoc_abc_output + 1 /\ sa_op_assoc_abc = 0) /\ sa_on_assoc_abc = S sd_half_assoc_abc_output)) /\ (sa_lp_assoc_abc + sa_rp_assoc_abc) + sa_on_assoc_abc = (sa_ln_assoc_abc + sa_rn_assoc_abc) + sa_op_assoc_abc)))) -> (exists sa_lp_assoc_bc sa_ln_assoc_bc sa_rp_assoc_bc sa_rn_assoc_bc sa_op_assoc_bc sa_on_assoc_bc. (((b = 2 * sa_lp_assoc_bc /\ sa_ln_assoc_bc = 0) \/ exists sd_half_assoc_bc_left. ((b = 2 * sd_half_assoc_bc_left + 1 /\ sa_lp_assoc_bc = 0) /\ sa_ln_assoc_bc = S sd_half_assoc_bc_left)) /\ (((c = 2 * sa_rp_assoc_bc /\ sa_rn_assoc_bc = 0) \/ exists sd_half_assoc_bc_right. ((c = 2 * sd_half_assoc_bc_right + 1 /\ sa_rp_assoc_bc = 0) /\ sa_rn_assoc_bc = S sd_half_assoc_bc_right)) /\ (((bc = 2 * sa_op_assoc_bc /\ sa_on_assoc_bc = 0) \/ exists sd_half_assoc_bc_output. ((bc = 2 * sd_half_assoc_bc_output + 1 /\ sa_op_assoc_bc = 0) /\ sa_on_assoc_bc = S sd_half_assoc_bc_output)) /\ (sa_lp_assoc_bc + sa_rp_assoc_bc) + sa_on_assoc_bc = (sa_ln_assoc_bc + sa_rn_assoc_bc) + sa_op_assoc_bc)))) -> (exists sa_lp_assoc_target sa_ln_assoc_target sa_rp_assoc_target sa_rn_assoc_target sa_op_assoc_target sa_on_assoc_target. (((a = 2 * sa_lp_assoc_target /\ sa_ln_assoc_target = 0) \/ exists sd_half_assoc_target_left. ((a = 2 * sd_half_assoc_target_left + 1 /\ sa_lp_assoc_target = 0) /\ sa_ln_assoc_target = S sd_half_assoc_target_left)) /\ (((bc = 2 * sa_rp_assoc_target /\ sa_rn_assoc_target = 0) \/ exists sd_half_assoc_target_right. ((bc = 2 * sd_half_assoc_target_right + 1 /\ sa_rp_assoc_target = 0) /\ sa_rn_assoc_target = S sd_half_assoc_target_right)) /\ (((abc = 2 * sa_op_assoc_target /\ sa_on_assoc_target = 0) \/ exists sd_half_assoc_target_output. ((abc = 2 * sd_half_assoc_target_output + 1 /\ sa_op_assoc_target = 0) /\ sa_on_assoc_target = S sd_half_assoc_target_output)) /\ (sa_lp_assoc_target + sa_rp_assoc_target) + sa_on_assoc_target = (sa_ln_assoc_target + sa_rn_assoc_target) + sa_op_assoc_target))))

signed_add_commutative · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right output. (exists sa_lp_comm_forward sa_ln_comm_forward sa_rp_comm_forward sa_rn_comm_forward sa_op_comm_forward sa_on_comm_forward. (((left = 2 * sa_lp_comm_forward /\ sa_ln_comm_forward = 0) \/ exists sd_half_comm_forward_left. ((left = 2 * sd_half_comm_forward_left + 1 /\ sa_lp_comm_forward = 0) /\ sa_ln_comm_forward = S sd_half_comm_forward_left)) /\ (((right = 2 * sa_rp_comm_forward /\ sa_rn_comm_forward = 0) \/ exists sd_half_comm_forward_right. ((right = 2 * sd_half_comm_forward_right + 1 /\ sa_rp_comm_forward = 0) /\ sa_rn_comm_forward = S sd_half_comm_forward_right)) /\ (((output = 2 * sa_op_comm_forward /\ sa_on_comm_forward = 0) \/ exists sd_half_comm_forward_output. ((output = 2 * sd_half_comm_forward_output + 1 /\ sa_op_comm_forward = 0) /\ sa_on_comm_forward = S sd_half_comm_forward_output)) /\ (sa_lp_comm_forward + sa_rp_comm_forward) + sa_on_comm_forward = (sa_ln_comm_forward + sa_rn_comm_forward) + sa_op_comm_forward)))) -> (exists sa_lp_comm_reverse sa_ln_comm_reverse sa_rp_comm_reverse sa_rn_comm_reverse sa_op_comm_reverse sa_on_comm_reverse. (((right = 2 * sa_lp_comm_reverse /\ sa_ln_comm_reverse = 0) \/ exists sd_half_comm_reverse_left. ((right = 2 * sd_half_comm_reverse_left + 1 /\ sa_lp_comm_reverse = 0) /\ sa_ln_comm_reverse = S sd_half_comm_reverse_left)) /\ (((left = 2 * sa_rp_comm_reverse /\ sa_rn_comm_reverse = 0) \/ exists sd_half_comm_reverse_right. ((left = 2 * sd_half_comm_reverse_right + 1 /\ sa_rp_comm_reverse = 0) /\ sa_rn_comm_reverse = S sd_half_comm_reverse_right)) /\ (((output = 2 * sa_op_comm_reverse /\ sa_on_comm_reverse = 0) \/ exists sd_half_comm_reverse_output. ((output = 2 * sd_half_comm_reverse_output + 1 /\ sa_op_comm_reverse = 0) /\ sa_on_comm_reverse = S sd_half_comm_reverse_output)) /\ (sa_lp_comm_reverse + sa_rp_comm_reverse) + sa_on_comm_reverse = (sa_ln_comm_reverse + sa_rn_comm_reverse) + sa_op_comm_reverse))))

signed_add_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right output1 output2. (exists sa_lp_functional_left sa_ln_functional_left sa_rp_functional_left sa_rn_functional_left sa_op_functional_left sa_on_functional_left. (((left = 2 * sa_lp_functional_left /\ sa_ln_functional_left = 0) \/ exists sd_half_functional_left_left. ((left = 2 * sd_half_functional_left_left + 1 /\ sa_lp_functional_left = 0) /\ sa_ln_functional_left = S sd_half_functional_left_left)) /\ (((right = 2 * sa_rp_functional_left /\ sa_rn_functional_left = 0) \/ exists sd_half_functional_left_right. ((right = 2 * sd_half_functional_left_right + 1 /\ sa_rp_functional_left = 0) /\ sa_rn_functional_left = S sd_half_functional_left_right)) /\ (((output1 = 2 * sa_op_functional_left /\ sa_on_functional_left = 0) \/ exists sd_half_functional_left_output. ((output1 = 2 * sd_half_functional_left_output + 1 /\ sa_op_functional_left = 0) /\ sa_on_functional_left = S sd_half_functional_left_output)) /\ (sa_lp_functional_left + sa_rp_functional_left) + sa_on_functional_left = (sa_ln_functional_left + sa_rn_functional_left) + sa_op_functional_left)))) -> (exists sa_lp_functional_right sa_ln_functional_right sa_rp_functional_right sa_rn_functional_right sa_op_functional_right sa_on_functional_right. (((left = 2 * sa_lp_functional_right /\ sa_ln_functional_right = 0) \/ exists sd_half_functional_right_left. ((left = 2 * sd_half_functional_right_left + 1 /\ sa_lp_functional_right = 0) /\ sa_ln_functional_right = S sd_half_functional_right_left)) /\ (((right = 2 * sa_rp_functional_right /\ sa_rn_functional_right = 0) \/ exists sd_half_functional_right_right. ((right = 2 * sd_half_functional_right_right + 1 /\ sa_rp_functional_right = 0) /\ sa_rn_functional_right = S sd_half_functional_right_right)) /\ (((output2 = 2 * sa_op_functional_right /\ sa_on_functional_right = 0) \/ exists sd_half_functional_right_output. ((output2 = 2 * sd_half_functional_right_output + 1 /\ sa_op_functional_right = 0) /\ sa_on_functional_right = S sd_half_functional_right_output)) /\ (sa_lp_functional_right + sa_rp_functional_right) + sa_on_functional_right = (sa_ln_functional_right + sa_rn_functional_right) + sa_op_functional_right)))) -> output1 = output2

signed_add_total · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right. exists output. (exists sa_lp_total sa_ln_total sa_rp_total sa_rn_total sa_op_total sa_on_total. (((left = 2 * sa_lp_total /\ sa_ln_total = 0) \/ exists sd_half_total_left. ((left = 2 * sd_half_total_left + 1 /\ sa_lp_total = 0) /\ sa_ln_total = S sd_half_total_left)) /\ (((right = 2 * sa_rp_total /\ sa_rn_total = 0) \/ exists sd_half_total_right. ((right = 2 * sd_half_total_right + 1 /\ sa_rp_total = 0) /\ sa_rn_total = S sd_half_total_right)) /\ (((output = 2 * sa_op_total /\ sa_on_total = 0) \/ exists sd_half_total_output. ((output = 2 * sd_half_total_output + 1 /\ sa_op_total = 0) /\ sa_on_total = S sd_half_total_output)) /\ (sa_lp_total + sa_rp_total) + sa_on_total = (sa_ln_total + sa_rn_total) + sa_op_total))))

signed_add_zero_left · checked inherited prerequisite

Exact statement in the checked dependency cone

forall input. (exists sa_lp_zero_left sa_ln_zero_left sa_rp_zero_left sa_rn_zero_left sa_op_zero_left sa_on_zero_left. (((0 = 2 * sa_lp_zero_left /\ sa_ln_zero_left = 0) \/ exists sd_half_zero_left_left. ((0 = 2 * sd_half_zero_left_left + 1 /\ sa_lp_zero_left = 0) /\ sa_ln_zero_left = S sd_half_zero_left_left)) /\ (((input = 2 * sa_rp_zero_left /\ sa_rn_zero_left = 0) \/ exists sd_half_zero_left_right. ((input = 2 * sd_half_zero_left_right + 1 /\ sa_rp_zero_left = 0) /\ sa_rn_zero_left = S sd_half_zero_left_right)) /\ (((input = 2 * sa_op_zero_left /\ sa_on_zero_left = 0) \/ exists sd_half_zero_left_output. ((input = 2 * sd_half_zero_left_output + 1 /\ sa_op_zero_left = 0) /\ sa_on_zero_left = S sd_half_zero_left_output)) /\ (sa_lp_zero_left + sa_rp_zero_left) + sa_on_zero_left = (sa_ln_zero_left + sa_rn_zero_left) + sa_op_zero_left))))

signed_mul_associative · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a b c ab bc abc. (exists sm_lp_assoc_ab sm_ln_assoc_ab sm_rp_assoc_ab sm_rn_assoc_ab sm_op_assoc_ab sm_on_assoc_ab. (((a = 2 * sm_lp_assoc_ab /\ sm_ln_assoc_ab = 0) \/ exists sd_half_assoc_ab_left. ((a = 2 * sd_half_assoc_ab_left + 1 /\ sm_lp_assoc_ab = 0) /\ sm_ln_assoc_ab = S sd_half_assoc_ab_left)) /\ (((b = 2 * sm_rp_assoc_ab /\ sm_rn_assoc_ab = 0) \/ exists sd_half_assoc_ab_right. ((b = 2 * sd_half_assoc_ab_right + 1 /\ sm_rp_assoc_ab = 0) /\ sm_rn_assoc_ab = S sd_half_assoc_ab_right)) /\ (((ab = 2 * sm_op_assoc_ab /\ sm_on_assoc_ab = 0) \/ exists sd_half_assoc_ab_output. ((ab = 2 * sd_half_assoc_ab_output + 1 /\ sm_op_assoc_ab = 0) /\ sm_on_assoc_ab = S sd_half_assoc_ab_output)) /\ (sm_lp_assoc_ab * sm_rp_assoc_ab + sm_ln_assoc_ab * sm_rn_assoc_ab) + sm_on_assoc_ab = (sm_lp_assoc_ab * sm_rn_assoc_ab + sm_ln_assoc_ab * sm_rp_assoc_ab) + sm_op_assoc_ab)))) -> (exists sm_lp_assoc_abc sm_ln_assoc_abc sm_rp_assoc_abc sm_rn_assoc_abc sm_op_assoc_abc sm_on_assoc_abc. (((ab = 2 * sm_lp_assoc_abc /\ sm_ln_assoc_abc = 0) \/ exists sd_half_assoc_abc_left. ((ab = 2 * sd_half_assoc_abc_left + 1 /\ sm_lp_assoc_abc = 0) /\ sm_ln_assoc_abc = S sd_half_assoc_abc_left)) /\ (((c = 2 * sm_rp_assoc_abc /\ sm_rn_assoc_abc = 0) \/ exists sd_half_assoc_abc_right. ((c = 2 * sd_half_assoc_abc_right + 1 /\ sm_rp_assoc_abc = 0) /\ sm_rn_assoc_abc = S sd_half_assoc_abc_right)) /\ (((abc = 2 * sm_op_assoc_abc /\ sm_on_assoc_abc = 0) \/ exists sd_half_assoc_abc_output. ((abc = 2 * sd_half_assoc_abc_output + 1 /\ sm_op_assoc_abc = 0) /\ sm_on_assoc_abc = S sd_half_assoc_abc_output)) /\ (sm_lp_assoc_abc * sm_rp_assoc_abc + sm_ln_assoc_abc * sm_rn_assoc_abc) + sm_on_assoc_abc = (sm_lp_assoc_abc * sm_rn_assoc_abc + sm_ln_assoc_abc * sm_rp_assoc_abc) + sm_op_assoc_abc)))) -> (exists sm_lp_assoc_bc sm_ln_assoc_bc sm_rp_assoc_bc sm_rn_assoc_bc sm_op_assoc_bc sm_on_assoc_bc. (((b = 2 * sm_lp_assoc_bc /\ sm_ln_assoc_bc = 0) \/ exists sd_half_assoc_bc_left. ((b = 2 * sd_half_assoc_bc_left + 1 /\ sm_lp_assoc_bc = 0) /\ sm_ln_assoc_bc = S sd_half_assoc_bc_left)) /\ (((c = 2 * sm_rp_assoc_bc /\ sm_rn_assoc_bc = 0) \/ exists sd_half_assoc_bc_right. ((c = 2 * sd_half_assoc_bc_right + 1 /\ sm_rp_assoc_bc = 0) /\ sm_rn_assoc_bc = S sd_half_assoc_bc_right)) /\ (((bc = 2 * sm_op_assoc_bc /\ sm_on_assoc_bc = 0) \/ exists sd_half_assoc_bc_output. ((bc = 2 * sd_half_assoc_bc_output + 1 /\ sm_op_assoc_bc = 0) /\ sm_on_assoc_bc = S sd_half_assoc_bc_output)) /\ (sm_lp_assoc_bc * sm_rp_assoc_bc + sm_ln_assoc_bc * sm_rn_assoc_bc) + sm_on_assoc_bc = (sm_lp_assoc_bc * sm_rn_assoc_bc + sm_ln_assoc_bc * sm_rp_assoc_bc) + sm_op_assoc_bc)))) -> (exists sm_lp_assoc_target sm_ln_assoc_target sm_rp_assoc_target sm_rn_assoc_target sm_op_assoc_target sm_on_assoc_target. (((a = 2 * sm_lp_assoc_target /\ sm_ln_assoc_target = 0) \/ exists sd_half_assoc_target_left. ((a = 2 * sd_half_assoc_target_left + 1 /\ sm_lp_assoc_target = 0) /\ sm_ln_assoc_target = S sd_half_assoc_target_left)) /\ (((bc = 2 * sm_rp_assoc_target /\ sm_rn_assoc_target = 0) \/ exists sd_half_assoc_target_right. ((bc = 2 * sd_half_assoc_target_right + 1 /\ sm_rp_assoc_target = 0) /\ sm_rn_assoc_target = S sd_half_assoc_target_right)) /\ (((abc = 2 * sm_op_assoc_target /\ sm_on_assoc_target = 0) \/ exists sd_half_assoc_target_output. ((abc = 2 * sd_half_assoc_target_output + 1 /\ sm_op_assoc_target = 0) /\ sm_on_assoc_target = S sd_half_assoc_target_output)) /\ (sm_lp_assoc_target * sm_rp_assoc_target + sm_ln_assoc_target * sm_rn_assoc_target) + sm_on_assoc_target = (sm_lp_assoc_target * sm_rn_assoc_target + sm_ln_assoc_target * sm_rp_assoc_target) + sm_op_assoc_target))))

signed_mul_commutative · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right output. (exists sm_lp_comm_forward sm_ln_comm_forward sm_rp_comm_forward sm_rn_comm_forward sm_op_comm_forward sm_on_comm_forward. (((left = 2 * sm_lp_comm_forward /\ sm_ln_comm_forward = 0) \/ exists sd_half_comm_forward_left. ((left = 2 * sd_half_comm_forward_left + 1 /\ sm_lp_comm_forward = 0) /\ sm_ln_comm_forward = S sd_half_comm_forward_left)) /\ (((right = 2 * sm_rp_comm_forward /\ sm_rn_comm_forward = 0) \/ exists sd_half_comm_forward_right. ((right = 2 * sd_half_comm_forward_right + 1 /\ sm_rp_comm_forward = 0) /\ sm_rn_comm_forward = S sd_half_comm_forward_right)) /\ (((output = 2 * sm_op_comm_forward /\ sm_on_comm_forward = 0) \/ exists sd_half_comm_forward_output. ((output = 2 * sd_half_comm_forward_output + 1 /\ sm_op_comm_forward = 0) /\ sm_on_comm_forward = S sd_half_comm_forward_output)) /\ (sm_lp_comm_forward * sm_rp_comm_forward + sm_ln_comm_forward * sm_rn_comm_forward) + sm_on_comm_forward = (sm_lp_comm_forward * sm_rn_comm_forward + sm_ln_comm_forward * sm_rp_comm_forward) + sm_op_comm_forward)))) -> (exists sm_lp_comm_reverse sm_ln_comm_reverse sm_rp_comm_reverse sm_rn_comm_reverse sm_op_comm_reverse sm_on_comm_reverse. (((right = 2 * sm_lp_comm_reverse /\ sm_ln_comm_reverse = 0) \/ exists sd_half_comm_reverse_left. ((right = 2 * sd_half_comm_reverse_left + 1 /\ sm_lp_comm_reverse = 0) /\ sm_ln_comm_reverse = S sd_half_comm_reverse_left)) /\ (((left = 2 * sm_rp_comm_reverse /\ sm_rn_comm_reverse = 0) \/ exists sd_half_comm_reverse_right. ((left = 2 * sd_half_comm_reverse_right + 1 /\ sm_rp_comm_reverse = 0) /\ sm_rn_comm_reverse = S sd_half_comm_reverse_right)) /\ (((output = 2 * sm_op_comm_reverse /\ sm_on_comm_reverse = 0) \/ exists sd_half_comm_reverse_output. ((output = 2 * sd_half_comm_reverse_output + 1 /\ sm_op_comm_reverse = 0) /\ sm_on_comm_reverse = S sd_half_comm_reverse_output)) /\ (sm_lp_comm_reverse * sm_rp_comm_reverse + sm_ln_comm_reverse * sm_rn_comm_reverse) + sm_on_comm_reverse = (sm_lp_comm_reverse * sm_rn_comm_reverse + sm_ln_comm_reverse * sm_rp_comm_reverse) + sm_op_comm_reverse))))

signed_mul_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right output1 output2. (exists sm_lp_functional_left sm_ln_functional_left sm_rp_functional_left sm_rn_functional_left sm_op_functional_left sm_on_functional_left. (((left = 2 * sm_lp_functional_left /\ sm_ln_functional_left = 0) \/ exists sd_half_functional_left_left. ((left = 2 * sd_half_functional_left_left + 1 /\ sm_lp_functional_left = 0) /\ sm_ln_functional_left = S sd_half_functional_left_left)) /\ (((right = 2 * sm_rp_functional_left /\ sm_rn_functional_left = 0) \/ exists sd_half_functional_left_right. ((right = 2 * sd_half_functional_left_right + 1 /\ sm_rp_functional_left = 0) /\ sm_rn_functional_left = S sd_half_functional_left_right)) /\ (((output1 = 2 * sm_op_functional_left /\ sm_on_functional_left = 0) \/ exists sd_half_functional_left_output. ((output1 = 2 * sd_half_functional_left_output + 1 /\ sm_op_functional_left = 0) /\ sm_on_functional_left = S sd_half_functional_left_output)) /\ (sm_lp_functional_left * sm_rp_functional_left + sm_ln_functional_left * sm_rn_functional_left) + sm_on_functional_left = (sm_lp_functional_left * sm_rn_functional_left + sm_ln_functional_left * sm_rp_functional_left) + sm_op_functional_left)))) -> (exists sm_lp_functional_right sm_ln_functional_right sm_rp_functional_right sm_rn_functional_right sm_op_functional_right sm_on_functional_right. (((left = 2 * sm_lp_functional_right /\ sm_ln_functional_right = 0) \/ exists sd_half_functional_right_left. ((left = 2 * sd_half_functional_right_left + 1 /\ sm_lp_functional_right = 0) /\ sm_ln_functional_right = S sd_half_functional_right_left)) /\ (((right = 2 * sm_rp_functional_right /\ sm_rn_functional_right = 0) \/ exists sd_half_functional_right_right. ((right = 2 * sd_half_functional_right_right + 1 /\ sm_rp_functional_right = 0) /\ sm_rn_functional_right = S sd_half_functional_right_right)) /\ (((output2 = 2 * sm_op_functional_right /\ sm_on_functional_right = 0) \/ exists sd_half_functional_right_output. ((output2 = 2 * sd_half_functional_right_output + 1 /\ sm_op_functional_right = 0) /\ sm_on_functional_right = S sd_half_functional_right_output)) /\ (sm_lp_functional_right * sm_rp_functional_right + sm_ln_functional_right * sm_rn_functional_right) + sm_on_functional_right = (sm_lp_functional_right * sm_rn_functional_right + sm_ln_functional_right * sm_rp_functional_right) + sm_op_functional_right)))) -> output1 = output2

signed_mul_left_distributive · checked inherited prerequisite

Exact statement in the checked dependency cone

forall a b c bc ab ac out. (exists sa_lp_distrib_left_bc sa_ln_distrib_left_bc sa_rp_distrib_left_bc sa_rn_distrib_left_bc sa_op_distrib_left_bc sa_on_distrib_left_bc. (((b = 2 * sa_lp_distrib_left_bc /\ sa_ln_distrib_left_bc = 0) \/ exists sd_half_distrib_left_bc_left. ((b = 2 * sd_half_distrib_left_bc_left + 1 /\ sa_lp_distrib_left_bc = 0) /\ sa_ln_distrib_left_bc = S sd_half_distrib_left_bc_left)) /\ (((c = 2 * sa_rp_distrib_left_bc /\ sa_rn_distrib_left_bc = 0) \/ exists sd_half_distrib_left_bc_right. ((c = 2 * sd_half_distrib_left_bc_right + 1 /\ sa_rp_distrib_left_bc = 0) /\ sa_rn_distrib_left_bc = S sd_half_distrib_left_bc_right)) /\ (((bc = 2 * sa_op_distrib_left_bc /\ sa_on_distrib_left_bc = 0) \/ exists sd_half_distrib_left_bc_output. ((bc = 2 * sd_half_distrib_left_bc_output + 1 /\ sa_op_distrib_left_bc = 0) /\ sa_on_distrib_left_bc = S sd_half_distrib_left_bc_output)) /\ (sa_lp_distrib_left_bc + sa_rp_distrib_left_bc) + sa_on_distrib_left_bc = (sa_ln_distrib_left_bc + sa_rn_distrib_left_bc) + sa_op_distrib_left_bc)))) -> (exists sm_lp_distrib_left_ab sm_ln_distrib_left_ab sm_rp_distrib_left_ab sm_rn_distrib_left_ab sm_op_distrib_left_ab sm_on_distrib_left_ab. (((a = 2 * sm_lp_distrib_left_ab /\ sm_ln_distrib_left_ab = 0) \/ exists sd_half_distrib_left_ab_left. ((a = 2 * sd_half_distrib_left_ab_left + 1 /\ sm_lp_distrib_left_ab = 0) /\ sm_ln_distrib_left_ab = S sd_half_distrib_left_ab_left)) /\ (((b = 2 * sm_rp_distrib_left_ab /\ sm_rn_distrib_left_ab = 0) \/ exists sd_half_distrib_left_ab_right. ((b = 2 * sd_half_distrib_left_ab_right + 1 /\ sm_rp_distrib_left_ab = 0) /\ sm_rn_distrib_left_ab = S sd_half_distrib_left_ab_right)) /\ (((ab = 2 * sm_op_distrib_left_ab /\ sm_on_distrib_left_ab = 0) \/ exists sd_half_distrib_left_ab_output. ((ab = 2 * sd_half_distrib_left_ab_output + 1 /\ sm_op_distrib_left_ab = 0) /\ sm_on_distrib_left_ab = S sd_half_distrib_left_ab_output)) /\ (sm_lp_distrib_left_ab * sm_rp_distrib_left_ab + sm_ln_distrib_left_ab * sm_rn_distrib_left_ab) + sm_on_distrib_left_ab = (sm_lp_distrib_left_ab * sm_rn_distrib_left_ab + sm_ln_distrib_left_ab * sm_rp_distrib_left_ab) + sm_op_distrib_left_ab)))) -> (exists sm_lp_distrib_left_ac sm_ln_distrib_left_ac sm_rp_distrib_left_ac sm_rn_distrib_left_ac sm_op_distrib_left_ac sm_on_distrib_left_ac. (((a = 2 * sm_lp_distrib_left_ac /\ sm_ln_distrib_left_ac = 0) \/ exists sd_half_distrib_left_ac_left. ((a = 2 * sd_half_distrib_left_ac_left + 1 /\ sm_lp_distrib_left_ac = 0) /\ sm_ln_distrib_left_ac = S sd_half_distrib_left_ac_left)) /\ (((c = 2 * sm_rp_distrib_left_ac /\ sm_rn_distrib_left_ac = 0) \/ exists sd_half_distrib_left_ac_right. ((c = 2 * sd_half_distrib_left_ac_right + 1 /\ sm_rp_distrib_left_ac = 0) /\ sm_rn_distrib_left_ac = S sd_half_distrib_left_ac_right)) /\ (((ac = 2 * sm_op_distrib_left_ac /\ sm_on_distrib_left_ac = 0) \/ exists sd_half_distrib_left_ac_output. ((ac = 2 * sd_half_distrib_left_ac_output + 1 /\ sm_op_distrib_left_ac = 0) /\ sm_on_distrib_left_ac = S sd_half_distrib_left_ac_output)) /\ (sm_lp_distrib_left_ac * sm_rp_distrib_left_ac + sm_ln_distrib_left_ac * sm_rn_distrib_left_ac) + sm_on_distrib_left_ac = (sm_lp_distrib_left_ac * sm_rn_distrib_left_ac + sm_ln_distrib_left_ac * sm_rp_distrib_left_ac) + sm_op_distrib_left_ac)))) -> (exists sm_lp_distrib_left_abc sm_ln_distrib_left_abc sm_rp_distrib_left_abc sm_rn_distrib_left_abc sm_op_distrib_left_abc sm_on_distrib_left_abc. (((a = 2 * sm_lp_distrib_left_abc /\ sm_ln_distrib_left_abc = 0) \/ exists sd_half_distrib_left_abc_left. ((a = 2 * sd_half_distrib_left_abc_left + 1 /\ sm_lp_distrib_left_abc = 0) /\ sm_ln_distrib_left_abc = S sd_half_distrib_left_abc_left)) /\ (((bc = 2 * sm_rp_distrib_left_abc /\ sm_rn_distrib_left_abc = 0) \/ exists sd_half_distrib_left_abc_right. ((bc = 2 * sd_half_distrib_left_abc_right + 1 /\ sm_rp_distrib_left_abc = 0) /\ sm_rn_distrib_left_abc = S sd_half_distrib_left_abc_right)) /\ (((out = 2 * sm_op_distrib_left_abc /\ sm_on_distrib_left_abc = 0) \/ exists sd_half_distrib_left_abc_output. ((out = 2 * sd_half_distrib_left_abc_output + 1 /\ sm_op_distrib_left_abc = 0) /\ sm_on_distrib_left_abc = S sd_half_distrib_left_abc_output)) /\ (sm_lp_distrib_left_abc * sm_rp_distrib_left_abc + sm_ln_distrib_left_abc * sm_rn_distrib_left_abc) + sm_on_distrib_left_abc = (sm_lp_distrib_left_abc * sm_rn_distrib_left_abc + sm_ln_distrib_left_abc * sm_rp_distrib_left_abc) + sm_op_distrib_left_abc)))) -> (exists sa_lp_distrib_left_products sa_ln_distrib_left_products sa_rp_distrib_left_products sa_rn_distrib_left_products sa_op_distrib_left_products sa_on_distrib_left_products. (((ab = 2 * sa_lp_distrib_left_products /\ sa_ln_distrib_left_products = 0) \/ exists sd_half_distrib_left_products_left. ((ab = 2 * sd_half_distrib_left_products_left + 1 /\ sa_lp_distrib_left_products = 0) /\ sa_ln_distrib_left_products = S sd_half_distrib_left_products_left)) /\ (((ac = 2 * sa_rp_distrib_left_products /\ sa_rn_distrib_left_products = 0) \/ exists sd_half_distrib_left_products_right. ((ac = 2 * sd_half_distrib_left_products_right + 1 /\ sa_rp_distrib_left_products = 0) /\ sa_rn_distrib_left_products = S sd_half_distrib_left_products_right)) /\ (((out = 2 * sa_op_distrib_left_products /\ sa_on_distrib_left_products = 0) \/ exists sd_half_distrib_left_products_output. ((out = 2 * sd_half_distrib_left_products_output + 1 /\ sa_op_distrib_left_products = 0) /\ sa_on_distrib_left_products = S sd_half_distrib_left_products_output)) /\ (sa_lp_distrib_left_products + sa_rp_distrib_left_products) + sa_on_distrib_left_products = (sa_ln_distrib_left_products + sa_rn_distrib_left_products) + sa_op_distrib_left_products))))

signed_mul_total · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right. exists output. (exists sm_lp_total sm_ln_total sm_rp_total sm_rn_total sm_op_total sm_on_total. (((left = 2 * sm_lp_total /\ sm_ln_total = 0) \/ exists sd_half_total_left. ((left = 2 * sd_half_total_left + 1 /\ sm_lp_total = 0) /\ sm_ln_total = S sd_half_total_left)) /\ (((right = 2 * sm_rp_total /\ sm_rn_total = 0) \/ exists sd_half_total_right. ((right = 2 * sd_half_total_right + 1 /\ sm_rp_total = 0) /\ sm_rn_total = S sd_half_total_right)) /\ (((output = 2 * sm_op_total /\ sm_on_total = 0) \/ exists sd_half_total_output. ((output = 2 * sd_half_total_output + 1 /\ sm_op_total = 0) /\ sm_on_total = S sd_half_total_output)) /\ (sm_lp_total * sm_rp_total + sm_ln_total * sm_rn_total) + sm_on_total = (sm_lp_total * sm_rn_total + sm_ln_total * sm_rp_total) + sm_op_total))))

signed_mul_zero_right · checked inherited prerequisite

Exact statement in the checked dependency cone

forall input. (exists sm_lp_zero_right sm_ln_zero_right sm_rp_zero_right sm_rn_zero_right sm_op_zero_right sm_on_zero_right. (((input = 2 * sm_lp_zero_right /\ sm_ln_zero_right = 0) \/ exists sd_half_zero_right_left. ((input = 2 * sd_half_zero_right_left + 1 /\ sm_lp_zero_right = 0) /\ sm_ln_zero_right = S sd_half_zero_right_left)) /\ (((0 = 2 * sm_rp_zero_right /\ sm_rn_zero_right = 0) \/ exists sd_half_zero_right_right. ((0 = 2 * sd_half_zero_right_right + 1 /\ sm_rp_zero_right = 0) /\ sm_rn_zero_right = S sd_half_zero_right_right)) /\ (((0 = 2 * sm_op_zero_right /\ sm_on_zero_right = 0) \/ exists sd_half_zero_right_output. ((0 = 2 * sd_half_zero_right_output + 1 /\ sm_op_zero_right = 0) /\ sm_on_zero_right = S sd_half_zero_right_output)) /\ (sm_lp_zero_right * sm_rp_zero_right + sm_ln_zero_right * sm_rn_zero_right) + sm_on_zero_right = (sm_lp_zero_right * sm_rn_zero_right + sm_ln_zero_right * sm_rp_zero_right) + sm_op_zero_right))))

succ_ne_zero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. ~(S n = 0)
```