Actual rectangular sums and finite Fubini — 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.

217 checked bundle nodes · 551 proof edges · 12534 body proof nodes.

Literal self-contained proof bundle · SHA-256 a6f62d8a0c89431b3596a0d15278643da6981afe166107cdc6aefa5433485395

signed_rectangular_slice_candidate.py · signed_rectangular_sums_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

RS0001 signed_rectangular_slice_lookup · actual bundle node 184
RS0002 signed_rectangular_slice_restrict · actual bundle node 185
RS0003 signed_rectangular_slice_empty · actual bundle node 186
RS0004 signed_rectangular_slice_extensional_unique · actual bundle node 187
RS0005 signed_rectangular_slice_extend · actual bundle node 188
RS0006 signed_rectangular_slice_exists · actual bundle node 189
RS0007 signed_rectangular_slice_exists_extensionally_unique · actual bundle node 190
RS0008 signed_rectangular_slice_sum_exists · actual bundle node 191
RS0009 signed_rectangular_slice_sum_functional · actual bundle node 192
RS000A signed_rectangular_slice_sum_empty_value · actual bundle node 193
RS000B signed_rectangular_slice_sum_empty_exists · actual bundle node 194
RS000C signed_rectangular_slice_sum_successor_decompose · actual bundle node 195
RS000D signed_rectangular_slice_sum_successor_intro · actual bundle node 196
RS000E signed_rectangular_slice_sum_successor_add · actual bundle node 197
RS000F signed_rectangular_slice_sum_exists_unique · actual bundle node 198
RS0010 signed_rectangular_row_sums_lookup · actual bundle node 199
RS0011 signed_rectangular_row_sums_restrict_outer · actual bundle node 200
RS0012 signed_rectangular_row_sums_empty · actual bundle node 201
RS0013 signed_rectangular_row_sums_extensional_unique · actual bundle node 202
RS0014 signed_rectangular_row_sums_extend · actual bundle node 203
RS0015 signed_rectangular_row_sums_exists · actual bundle node 204
RS0016 signed_rectangular_row_sums_exists_extensionally_unique · actual bundle node 205
RS0017 signed_rectangular_sum_exists · actual bundle node 206
RS0018 signed_rectangular_sum_functional · actual bundle node 207
RS0019 signed_rectangular_sum_exists_unique · actual bundle node 208
RS001A signed_rectangular_sum_zero_outer · actual bundle node 209
RS001B signed_rectangular_row_sums_zero_inner · actual bundle node 210
RS001C signed_rectangular_sum_zero_inner · actual bundle node 211
RS001D signed_rectangular_columns_successor_add · actual bundle node 212
RS001E signed_rectangular_fubini · actual bundle node 213
RS001F signed_rectangular_fubini_exists · actual bundle node 214
RS0020 signed_rectangular_row_major_fubini · actual bundle node 215
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_append_transport · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F G l a b c. (exists dst_positive_code_append_sum_valid dst_positive_scale_append_sum_valid dst_negative_code_append_sum_valid dst_negative_scale_append_sum_valid. (((G) = (((((dst_positive_code_append_sum_valid) + (dst_positive_scale_append_sum_valid)) * S ((dst_positive_code_append_sum_valid) + (dst_positive_scale_append_sum_valid)) + ((dst_positive_scale_append_sum_valid) + (dst_positive_scale_append_sum_valid))) + (((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) * S ((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) + ((dst_negative_scale_append_sum_valid) + (dst_negative_scale_append_sum_valid)))) * S ((((dst_positive_code_append_sum_valid) + (dst_positive_scale_append_sum_valid)) * S ((dst_positive_code_append_sum_valid) + (dst_positive_scale_append_sum_valid)) + ((dst_positive_scale_append_sum_valid) + (dst_positive_scale_append_sum_valid))) + (((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) * S ((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) + ((dst_negative_scale_append_sum_valid) + (dst_negative_scale_append_sum_valid)))) + ((((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) * S ((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) + ((dst_negative_scale_append_sum_valid) + (dst_negative_scale_append_sum_valid))) + (((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) * S ((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) + ((dst_negative_scale_append_sum_valid) + (dst_negative_scale_append_sum_valid)))))) /\ (forall dst_index_append_sum_valid. (exists pvs_le_gap_append_sum_validdomain. pvs_le_gap_append_sum_validdomain + (dst_index_append_sum_valid) = (l)) -> exists dst_positive_append_sum_valid dst_negative_append_sum_valid dst_value_append_sum_valid. ((((exists ff_h_pvs_append_sum_validentrypositive. ff_h_pvs_append_sum_validentrypositive + S (dst_positive_append_sum_valid) = S ((S (dst_index_append_sum_valid)) * dst_positive_scale_append_sum_valid)) /\ exists ff_q_pvs_append_sum_validentrypositive. dst_positive_code_append_sum_valid = ff_q_pvs_append_sum_validentrypositive * S ((S (dst_index_append_sum_valid)) * dst_positive_scale_append_sum_valid) + (dst_positive_append_sum_valid))) /\ (((((exists ff_h_pvs_append_sum_validentrynegative. ff_h_pvs_append_sum_validentrynegative + S (dst_negative_append_sum_valid) = S ((S (dst_index_append_sum_valid)) * dst_negative_scale_append_sum_valid)) /\ exists ff_q_pvs_append_sum_validentrynegative. dst_negative_code_append_sum_valid = ff_q_pvs_append_sum_validentrynegative * S ((S (dst_index_append_sum_valid)) * dst_negative_scale_append_sum_valid) + (dst_negative_append_sum_valid))) /\ (exists ge_balance_positive_append_sum_validentryvalue ge_balance_negative_append_sum_validentryvalue. (((((dst_value_append_sum_valid) = 2 * (ge_balance_positive_append_sum_validentryvalue) /\ (ge_balance_negative_append_sum_validentryvalue) = 0) \/ exists ge_signed_half_append_sum_validentryvaluedecode. (((dst_value_append_sum_valid) = 2 * ge_signed_half_append_sum_validentryvaluedecode + 1 /\ (ge_balance_positive_append_sum_validentryvalue) = 0) /\ (ge_balance_negative_append_sum_validentryvalue) = S ge_signed_half_append_sum_validentryvaluedecode))) /\ ((dst_positive_append_sum_valid) + ge_balance_negative_append_sum_validentryvalue = (dst_negative_append_sum_valid) + ge_balance_positive_append_sum_validentryvalue))))))))) -> (forall dst_index_append_sum_prefix dst_first_append_sum_prefix dst_second_append_sum_prefix. (exists pvs_gap_append_sum_prefixbound. pvs_gap_append_sum_prefixbound + S (dst_index_append_sum_prefix) = (l)) -> (exists dst_positive_code_append_sum_prefixfirst dst_positive_scale_append_sum_prefixfirst dst_negative_code_append_sum_prefixfirst dst_negative_scale_append_sum_prefixfirst dst_positive_append_sum_prefixfirst dst_negative_append_sum_prefixfirst. (((F) = (((((dst_positive_code_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst)) * S ((dst_positive_code_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst)) + ((dst_positive_scale_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst))) + (((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) * S ((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) + ((dst_negative_scale_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)))) * S ((((dst_positive_code_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst)) * S ((dst_positive_code_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst)) + ((dst_positive_scale_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst))) + (((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) * S ((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) + ((dst_negative_scale_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)))) + ((((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) * S ((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) + ((dst_negative_scale_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst))) + (((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) * S ((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) + ((dst_negative_scale_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)))))) /\ (((((exists ff_h_pvs_append_sum_prefixfirstpositive. ff_h_pvs_append_sum_prefixfirstpositive + S (dst_positive_append_sum_prefixfirst) = S ((S (dst_index_append_sum_prefix)) * dst_positive_scale_append_sum_prefixfirst)) /\ exists ff_q_pvs_append_sum_prefixfirstpositive. dst_positive_code_append_sum_prefixfirst = ff_q_pvs_append_sum_prefixfirstpositive * S ((S (dst_index_append_sum_prefix)) * dst_positive_scale_append_sum_prefixfirst) + (dst_positive_append_sum_prefixfirst))) /\ (((((exists ff_h_pvs_append_sum_prefixfirstnegative. ff_h_pvs_append_sum_prefixfirstnegative + S (dst_negative_append_sum_prefixfirst) = S ((S (dst_index_append_sum_prefix)) * dst_negative_scale_append_sum_prefixfirst)) /\ exists ff_q_pvs_append_sum_prefixfirstnegative. dst_negative_code_append_sum_prefixfirst = ff_q_pvs_append_sum_prefixfirstnegative * S ((S (dst_index_append_sum_prefix)) * dst_negative_scale_append_sum_prefixfirst) + (dst_negative_append_sum_prefixfirst))) /\ (exists ge_balance_positive_append_sum_prefixfirstvalue ge_balance_negative_append_sum_prefixfirstvalue. (((((dst_first_append_sum_prefix) = 2 * (ge_balance_positive_append_sum_prefixfirstvalue) /\ (ge_balance_negative_append_sum_prefixfirstvalue) = 0) \/ exists ge_signed_half_append_sum_prefixfirstvaluedecode. (((dst_first_append_sum_prefix) = 2 * ge_signed_half_append_sum_prefixfirstvaluedecode + 1 /\ (ge_balance_positive_append_sum_prefixfirstvalue) = 0) /\ (ge_balance_negative_append_sum_prefixfirstvalue) = S ge_signed_half_append_sum_prefixfirstvaluedecode))) /\ ((dst_positive_append_sum_prefixfirst) + ge_balance_negative_append_sum_prefixfirstvalue = (dst_negative_append_sum_prefixfirst) + ge_balance_positive_append_sum_prefixfirstvalue))))))))) -> (exists dst_positive_code_append_sum_prefixsecond dst_positive_scale_append_sum_prefixsecond dst_negative_code_append_sum_prefixsecond dst_negative_scale_append_sum_prefixsecond dst_positive_append_sum_prefixsecond dst_negative_append_sum_prefixsecond. (((G) = (((((dst_positive_code_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond)) * S ((dst_positive_code_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond)) + ((dst_positive_scale_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond))) + (((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) * S ((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) + ((dst_negative_scale_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)))) * S ((((dst_positive_code_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond)) * S ((dst_positive_code_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond)) + ((dst_positive_scale_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond))) + (((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) * S ((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) + ((dst_negative_scale_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)))) + ((((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) * S ((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) + ((dst_negative_scale_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond))) + (((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) * S ((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) + ((dst_negative_scale_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)))))) /\ (((((exists ff_h_pvs_append_sum_prefixsecondpositive. ff_h_pvs_append_sum_prefixsecondpositive + S (dst_positive_append_sum_prefixsecond) = S ((S (dst_index_append_sum_prefix)) * dst_positive_scale_append_sum_prefixsecond)) /\ exists ff_q_pvs_append_sum_prefixsecondpositive. dst_positive_code_append_sum_prefixsecond = ff_q_pvs_append_sum_prefixsecondpositive * S ((S (dst_index_append_sum_prefix)) * dst_positive_scale_append_sum_prefixsecond) + (dst_positive_append_sum_prefixsecond))) /\ (((((exists ff_h_pvs_append_sum_prefixsecondnegative. ff_h_pvs_append_sum_prefixsecondnegative + S (dst_negative_append_sum_prefixsecond) = S ((S (dst_index_append_sum_prefix)) * dst_negative_scale_append_sum_prefixsecond)) /\ exists ff_q_pvs_append_sum_prefixsecondnegative. dst_negative_code_append_sum_prefixsecond = ff_q_pvs_append_sum_prefixsecondnegative * S ((S (dst_index_append_sum_prefix)) * dst_negative_scale_append_sum_prefixsecond) + (dst_negative_append_sum_prefixsecond))) /\ (exists ge_balance_positive_append_sum_prefixsecondvalue ge_balance_negative_append_sum_prefixsecondvalue. (((((dst_second_append_sum_prefix) = 2 * (ge_balance_positive_append_sum_prefixsecondvalue) /\ (ge_balance_negative_append_sum_prefixsecondvalue) = 0) \/ exists ge_signed_half_append_sum_prefixsecondvaluedecode. (((dst_second_append_sum_prefix) = 2 * ge_signed_half_append_sum_prefixsecondvaluedecode + 1 /\ (ge_balance_positive_append_sum_prefixsecondvalue) = 0) /\ (ge_balance_negative_append_sum_prefixsecondvalue) = S ge_signed_half_append_sum_prefixsecondvaluedecode))) /\ ((dst_positive_append_sum_prefixsecond) + ge_balance_negative_append_sum_prefixsecondvalue = (dst_negative_append_sum_prefixsecond) + ge_balance_positive_append_sum_prefixsecondvalue))))))))) -> dst_first_append_sum_prefix = dst_second_append_sum_prefix) -> (exists dst_positive_code_append_sum_before dst_positive_scale_append_sum_before dst_negative_code_append_sum_before dst_negative_scale_append_sum_before dst_positive_sum_append_sum_before dst_negative_sum_append_sum_before. (((F) = (((((dst_positive_code_append_sum_before) + (dst_positive_scale_append_sum_before)) * S ((dst_positive_code_append_sum_before) + (dst_positive_scale_append_sum_before)) + ((dst_positive_scale_append_sum_before) + (dst_positive_scale_append_sum_before))) + (((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) * S ((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) + ((dst_negative_scale_append_sum_before) + (dst_negative_scale_append_sum_before)))) * S ((((dst_positive_code_append_sum_before) + (dst_positive_scale_append_sum_before)) * S ((dst_positive_code_append_sum_before) + (dst_positive_scale_append_sum_before)) + ((dst_positive_scale_append_sum_before) + (dst_positive_scale_append_sum_before))) + (((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) * S ((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) + ((dst_negative_scale_append_sum_before) + (dst_negative_scale_append_sum_before)))) + ((((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) * S ((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) + ((dst_negative_scale_append_sum_before) + (dst_negative_scale_append_sum_before))) + (((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) * S ((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) + ((dst_negative_scale_append_sum_before) + (dst_negative_scale_append_sum_before)))))) /\ (((exists fs_u_dst_append_sum_beforepositive fs_v_dst_append_sum_beforepositive. ((((exists fs_h_dst_append_sum_beforepositive_body_start. fs_h_dst_append_sum_beforepositive_body_start + S (0) = S ((S (0)) * fs_v_dst_append_sum_beforepositive)) /\ exists fs_q_dst_append_sum_beforepositive_body_start. fs_u_dst_append_sum_beforepositive = fs_q_dst_append_sum_beforepositive_body_start * S ((S (0)) * fs_v_dst_append_sum_beforepositive) + (0))) /\ ((((exists fs_h_dst_append_sum_beforepositive_body_terminal. fs_h_dst_append_sum_beforepositive_body_terminal + S (dst_positive_sum_append_sum_before) = S ((S (l)) * fs_v_dst_append_sum_beforepositive)) /\ exists fs_q_dst_append_sum_beforepositive_body_terminal. fs_u_dst_append_sum_beforepositive = fs_q_dst_append_sum_beforepositive_body_terminal * S ((S (l)) * fs_v_dst_append_sum_beforepositive) + (dst_positive_sum_append_sum_before))) /\ forall fs_i_dst_append_sum_beforepositive_body_steps. (exists fs_lt_dst_append_sum_beforepositive_body_steps_bound. fs_lt_dst_append_sum_beforepositive_body_steps_bound + S fs_i_dst_append_sum_beforepositive_body_steps = l) -> exists fs_a_dst_append_sum_beforepositive_body_steps fs_r_dst_append_sum_beforepositive_body_steps fs_s_dst_append_sum_beforepositive_body_steps. ((((exists fs_h_dst_append_sum_beforepositive_body_steps_summand. fs_h_dst_append_sum_beforepositive_body_steps_summand + S (fs_a_dst_append_sum_beforepositive_body_steps) = S ((S (fs_i_dst_append_sum_beforepositive_body_steps)) * dst_positive_scale_append_sum_before)) /\ exists fs_q_dst_append_sum_beforepositive_body_steps_summand. dst_positive_code_append_sum_before = fs_q_dst_append_sum_beforepositive_body_steps_summand * S ((S (fs_i_dst_append_sum_beforepositive_body_steps)) * dst_positive_scale_append_sum_before) + (fs_a_dst_append_sum_beforepositive_body_steps))) /\ ((((exists fs_h_dst_append_sum_beforepositive_body_steps_partial. fs_h_dst_append_sum_beforepositive_body_steps_partial + S (fs_r_dst_append_sum_beforepositive_body_steps) = S ((S (fs_i_dst_append_sum_beforepositive_body_steps)) * fs_v_dst_append_sum_beforepositive)) /\ exists fs_q_dst_append_sum_beforepositive_body_steps_partial. fs_u_dst_append_sum_beforepositive = fs_q_dst_append_sum_beforepositive_body_steps_partial * S ((S (fs_i_dst_append_sum_beforepositive_body_steps)) * fs_v_dst_append_sum_beforepositive) + (fs_r_dst_append_sum_beforepositive_body_steps))) /\ ((((exists fs_h_dst_append_sum_beforepositive_body_steps_successor. fs_h_dst_append_sum_beforepositive_body_steps_successor + S (fs_s_dst_append_sum_beforepositive_body_steps) = S ((S (S fs_i_dst_append_sum_beforepositive_body_steps)) * fs_v_dst_append_sum_beforepositive)) /\ exists fs_q_dst_append_sum_beforepositive_body_steps_successor. fs_u_dst_append_sum_beforepositive = fs_q_dst_append_sum_beforepositive_body_steps_successor * S ((S (S fs_i_dst_append_sum_beforepositive_body_steps)) * fs_v_dst_append_sum_beforepositive) + (fs_s_dst_append_sum_beforepositive_body_steps))) /\ fs_s_dst_append_sum_beforepositive_body_steps = fs_r_dst_append_sum_beforepositive_body_steps + fs_a_dst_append_sum_beforepositive_body_steps)))))) /\ (((exists fs_u_dst_append_sum_beforenegative fs_v_dst_append_sum_beforenegative. ((((exists fs_h_dst_append_sum_beforenegative_body_start. fs_h_dst_append_sum_beforenegative_body_start + S (0) = S ((S (0)) * fs_v_dst_append_sum_beforenegative)) /\ exists fs_q_dst_append_sum_beforenegative_body_start. fs_u_dst_append_sum_beforenegative = fs_q_dst_append_sum_beforenegative_body_start * S ((S (0)) * fs_v_dst_append_sum_beforenegative) + (0))) /\ ((((exists fs_h_dst_append_sum_beforenegative_body_terminal. fs_h_dst_append_sum_beforenegative_body_terminal + S (dst_negative_sum_append_sum_before) = S ((S (l)) * fs_v_dst_append_sum_beforenegative)) /\ exists fs_q_dst_append_sum_beforenegative_body_terminal. fs_u_dst_append_sum_beforenegative = fs_q_dst_append_sum_beforenegative_body_terminal * S ((S (l)) * fs_v_dst_append_sum_beforenegative) + (dst_negative_sum_append_sum_before))) /\ forall fs_i_dst_append_sum_beforenegative_body_steps. (exists fs_lt_dst_append_sum_beforenegative_body_steps_bound. fs_lt_dst_append_sum_beforenegative_body_steps_bound + S fs_i_dst_append_sum_beforenegative_body_steps = l) -> exists fs_a_dst_append_sum_beforenegative_body_steps fs_r_dst_append_sum_beforenegative_body_steps fs_s_dst_append_sum_beforenegative_body_steps. ((((exists fs_h_dst_append_sum_beforenegative_body_steps_summand. fs_h_dst_append_sum_beforenegative_body_steps_summand + S (fs_a_dst_append_sum_beforenegative_body_steps) = S ((S (fs_i_dst_append_sum_beforenegative_body_steps)) * dst_negative_scale_append_sum_before)) /\ exists fs_q_dst_append_sum_beforenegative_body_steps_summand. dst_negative_code_append_sum_before = fs_q_dst_append_sum_beforenegative_body_steps_summand * S ((S (fs_i_dst_append_sum_beforenegative_body_steps)) * dst_negative_scale_append_sum_before) + (fs_a_dst_append_sum_beforenegative_body_steps))) /\ ((((exists fs_h_dst_append_sum_beforenegative_body_steps_partial. fs_h_dst_append_sum_beforenegative_body_steps_partial + S (fs_r_dst_append_sum_beforenegative_body_steps) = S ((S (fs_i_dst_append_sum_beforenegative_body_steps)) * fs_v_dst_append_sum_beforenegative)) /\ exists fs_q_dst_append_sum_beforenegative_body_steps_partial. fs_u_dst_append_sum_beforenegative = fs_q_dst_append_sum_beforenegative_body_steps_partial * S ((S (fs_i_dst_append_sum_beforenegative_body_steps)) * fs_v_dst_append_sum_beforenegative) + (fs_r_dst_append_sum_beforenegative_body_steps))) /\ ((((exists fs_h_dst_append_sum_beforenegative_body_steps_successor. fs_h_dst_append_sum_beforenegative_body_steps_successor + S (fs_s_dst_append_sum_beforenegative_body_steps) = S ((S (S fs_i_dst_append_sum_beforenegative_body_steps)) * fs_v_dst_append_sum_beforenegative)) /\ exists fs_q_dst_append_sum_beforenegative_body_steps_successor. fs_u_dst_append_sum_beforenegative = fs_q_dst_append_sum_beforenegative_body_steps_successor * S ((S (S fs_i_dst_append_sum_beforenegative_body_steps)) * fs_v_dst_append_sum_beforenegative) + (fs_s_dst_append_sum_beforenegative_body_steps))) /\ fs_s_dst_append_sum_beforenegative_body_steps = fs_r_dst_append_sum_beforenegative_body_steps + fs_a_dst_append_sum_beforenegative_body_steps)))))) /\ (exists ge_balance_positive_append_sum_beforeresult ge_balance_negative_append_sum_beforeresult. (((((a) = 2 * (ge_balance_positive_append_sum_beforeresult) /\ (ge_balance_negative_append_sum_beforeresult) = 0) \/ exists ge_signed_half_append_sum_beforeresultdecode. (((a) = 2 * ge_signed_half_append_sum_beforeresultdecode + 1 /\ (ge_balance_positive_append_sum_beforeresult) = 0) /\ (ge_balance_negative_append_sum_beforeresult) = S ge_signed_half_append_sum_beforeresultdecode))) /\ ((dst_positive_sum_append_sum_before) + ge_balance_negative_append_sum_beforeresult = (dst_negative_sum_append_sum_before) + ge_balance_positive_append_sum_beforeresult))))))))) -> (exists dst_positive_code_append_sum_entry dst_positive_scale_append_sum_entry dst_negative_code_append_sum_entry dst_negative_scale_append_sum_entry dst_positive_append_sum_entry dst_negative_append_sum_entry. (((G) = (((((dst_positive_code_append_sum_entry) + (dst_positive_scale_append_sum_entry)) * S ((dst_positive_code_append_sum_entry) + (dst_positive_scale_append_sum_entry)) + ((dst_positive_scale_append_sum_entry) + (dst_positive_scale_append_sum_entry))) + (((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) * S ((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) + ((dst_negative_scale_append_sum_entry) + (dst_negative_scale_append_sum_entry)))) * S ((((dst_positive_code_append_sum_entry) + (dst_positive_scale_append_sum_entry)) * S ((dst_positive_code_append_sum_entry) + (dst_positive_scale_append_sum_entry)) + ((dst_positive_scale_append_sum_entry) + (dst_positive_scale_append_sum_entry))) + (((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) * S ((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) + ((dst_negative_scale_append_sum_entry) + (dst_negative_scale_append_sum_entry)))) + ((((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) * S ((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) + ((dst_negative_scale_append_sum_entry) + (dst_negative_scale_append_sum_entry))) + (((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) * S ((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) + ((dst_negative_scale_append_sum_entry) + (dst_negative_scale_append_sum_entry)))))) /\ (((((exists ff_h_pvs_append_sum_entrypositive. ff_h_pvs_append_sum_entrypositive + S (dst_positive_append_sum_entry) = S ((S (l)) * dst_positive_scale_append_sum_entry)) /\ exists ff_q_pvs_append_sum_entrypositive. dst_positive_code_append_sum_entry = ff_q_pvs_append_sum_entrypositive * S ((S (l)) * dst_positive_scale_append_sum_entry) + (dst_positive_append_sum_entry))) /\ (((((exists ff_h_pvs_append_sum_entrynegative. ff_h_pvs_append_sum_entrynegative + S (dst_negative_append_sum_entry) = S ((S (l)) * dst_negative_scale_append_sum_entry)) /\ exists ff_q_pvs_append_sum_entrynegative. dst_negative_code_append_sum_entry = ff_q_pvs_append_sum_entrynegative * S ((S (l)) * dst_negative_scale_append_sum_entry) + (dst_negative_append_sum_entry))) /\ (exists ge_balance_positive_append_sum_entryvalue ge_balance_negative_append_sum_entryvalue. (((((b) = 2 * (ge_balance_positive_append_sum_entryvalue) /\ (ge_balance_negative_append_sum_entryvalue) = 0) \/ exists ge_signed_half_append_sum_entryvaluedecode. (((b) = 2 * ge_signed_half_append_sum_entryvaluedecode + 1 /\ (ge_balance_positive_append_sum_entryvalue) = 0) /\ (ge_balance_negative_append_sum_entryvalue) = S ge_signed_half_append_sum_entryvaluedecode))) /\ ((dst_positive_append_sum_entry) + ge_balance_negative_append_sum_entryvalue = (dst_negative_append_sum_entry) + ge_balance_positive_append_sum_entryvalue))))))))) -> (exists dsa_ap_append_sum_add dsa_an_append_sum_add dsa_bp_append_sum_add dsa_bn_append_sum_add dsa_cp_append_sum_add dsa_cn_append_sum_add. (((((a) = 2 * (dsa_ap_append_sum_add) /\ (dsa_an_append_sum_add) = 0) \/ exists ge_signed_half_append_sum_addleft. (((a) = 2 * ge_signed_half_append_sum_addleft + 1 /\ (dsa_ap_append_sum_add) = 0) /\ (dsa_an_append_sum_add) = S ge_signed_half_append_sum_addleft))) /\ ((((((b) = 2 * (dsa_bp_append_sum_add) /\ (dsa_bn_append_sum_add) = 0) \/ exists ge_signed_half_append_sum_addright. (((b) = 2 * ge_signed_half_append_sum_addright + 1 /\ (dsa_bp_append_sum_add) = 0) /\ (dsa_bn_append_sum_add) = S ge_signed_half_append_sum_addright))) /\ ((((((c) = 2 * (dsa_cp_append_sum_add) /\ (dsa_cn_append_sum_add) = 0) \/ exists ge_signed_half_append_sum_addoutput. (((c) = 2 * ge_signed_half_append_sum_addoutput + 1 /\ (dsa_cp_append_sum_add) = 0) /\ (dsa_cn_append_sum_add) = S ge_signed_half_append_sum_addoutput))) /\ ((dsa_ap_append_sum_add + dsa_bp_append_sum_add) + dsa_cn_append_sum_add = (dsa_an_append_sum_add + dsa_bn_append_sum_add) + dsa_cp_append_sum_add))))))) -> (exists dst_positive_code_append_sum_result dst_positive_scale_append_sum_result dst_negative_code_append_sum_result dst_negative_scale_append_sum_result dst_positive_sum_append_sum_result dst_negative_sum_append_sum_result. (((G) = (((((dst_positive_code_append_sum_result) + (dst_positive_scale_append_sum_result)) * S ((dst_positive_code_append_sum_result) + (dst_positive_scale_append_sum_result)) + ((dst_positive_scale_append_sum_result) + (dst_positive_scale_append_sum_result))) + (((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) * S ((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) + ((dst_negative_scale_append_sum_result) + (dst_negative_scale_append_sum_result)))) * S ((((dst_positive_code_append_sum_result) + (dst_positive_scale_append_sum_result)) * S ((dst_positive_code_append_sum_result) + (dst_positive_scale_append_sum_result)) + ((dst_positive_scale_append_sum_result) + (dst_positive_scale_append_sum_result))) + (((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) * S ((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) + ((dst_negative_scale_append_sum_result) + (dst_negative_scale_append_sum_result)))) + ((((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) * S ((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) + ((dst_negative_scale_append_sum_result) + (dst_negative_scale_append_sum_result))) + (((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) * S ((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) + ((dst_negative_scale_append_sum_result) + (dst_negative_scale_append_sum_result)))))) /\ (((exists fs_u_dst_append_sum_resultpositive fs_v_dst_append_sum_resultpositive. ((((exists fs_h_dst_append_sum_resultpositive_body_start. fs_h_dst_append_sum_resultpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_append_sum_resultpositive)) /\ exists fs_q_dst_append_sum_resultpositive_body_start. fs_u_dst_append_sum_resultpositive = fs_q_dst_append_sum_resultpositive_body_start * S ((S (0)) * fs_v_dst_append_sum_resultpositive) + (0))) /\ ((((exists fs_h_dst_append_sum_resultpositive_body_terminal. fs_h_dst_append_sum_resultpositive_body_terminal + S (dst_positive_sum_append_sum_result) = S ((S (S l)) * fs_v_dst_append_sum_resultpositive)) /\ exists fs_q_dst_append_sum_resultpositive_body_terminal. fs_u_dst_append_sum_resultpositive = fs_q_dst_append_sum_resultpositive_body_terminal * S ((S (S l)) * fs_v_dst_append_sum_resultpositive) + (dst_positive_sum_append_sum_result))) /\ forall fs_i_dst_append_sum_resultpositive_body_steps. (exists fs_lt_dst_append_sum_resultpositive_body_steps_bound. fs_lt_dst_append_sum_resultpositive_body_steps_bound + S fs_i_dst_append_sum_resultpositive_body_steps = S l) -> exists fs_a_dst_append_sum_resultpositive_body_steps fs_r_dst_append_sum_resultpositive_body_steps fs_s_dst_append_sum_resultpositive_body_steps. ((((exists fs_h_dst_append_sum_resultpositive_body_steps_summand. fs_h_dst_append_sum_resultpositive_body_steps_summand + S (fs_a_dst_append_sum_resultpositive_body_steps) = S ((S (fs_i_dst_append_sum_resultpositive_body_steps)) * dst_positive_scale_append_sum_result)) /\ exists fs_q_dst_append_sum_resultpositive_body_steps_summand. dst_positive_code_append_sum_result = fs_q_dst_append_sum_resultpositive_body_steps_summand * S ((S (fs_i_dst_append_sum_resultpositive_body_steps)) * dst_positive_scale_append_sum_result) + (fs_a_dst_append_sum_resultpositive_body_steps))) /\ ((((exists fs_h_dst_append_sum_resultpositive_body_steps_partial. fs_h_dst_append_sum_resultpositive_body_steps_partial + S (fs_r_dst_append_sum_resultpositive_body_steps) = S ((S (fs_i_dst_append_sum_resultpositive_body_steps)) * fs_v_dst_append_sum_resultpositive)) /\ exists fs_q_dst_append_sum_resultpositive_body_steps_partial. fs_u_dst_append_sum_resultpositive = fs_q_dst_append_sum_resultpositive_body_steps_partial * S ((S (fs_i_dst_append_sum_resultpositive_body_steps)) * fs_v_dst_append_sum_resultpositive) + (fs_r_dst_append_sum_resultpositive_body_steps))) /\ ((((exists fs_h_dst_append_sum_resultpositive_body_steps_successor. fs_h_dst_append_sum_resultpositive_body_steps_successor + S (fs_s_dst_append_sum_resultpositive_body_steps) = S ((S (S fs_i_dst_append_sum_resultpositive_body_steps)) * fs_v_dst_append_sum_resultpositive)) /\ exists fs_q_dst_append_sum_resultpositive_body_steps_successor. fs_u_dst_append_sum_resultpositive = fs_q_dst_append_sum_resultpositive_body_steps_successor * S ((S (S fs_i_dst_append_sum_resultpositive_body_steps)) * fs_v_dst_append_sum_resultpositive) + (fs_s_dst_append_sum_resultpositive_body_steps))) /\ fs_s_dst_append_sum_resultpositive_body_steps = fs_r_dst_append_sum_resultpositive_body_steps + fs_a_dst_append_sum_resultpositive_body_steps)))))) /\ (((exists fs_u_dst_append_sum_resultnegative fs_v_dst_append_sum_resultnegative. ((((exists fs_h_dst_append_sum_resultnegative_body_start. fs_h_dst_append_sum_resultnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_append_sum_resultnegative)) /\ exists fs_q_dst_append_sum_resultnegative_body_start. fs_u_dst_append_sum_resultnegative = fs_q_dst_append_sum_resultnegative_body_start * S ((S (0)) * fs_v_dst_append_sum_resultnegative) + (0))) /\ ((((exists fs_h_dst_append_sum_resultnegative_body_terminal. fs_h_dst_append_sum_resultnegative_body_terminal + S (dst_negative_sum_append_sum_result) = S ((S (S l)) * fs_v_dst_append_sum_resultnegative)) /\ exists fs_q_dst_append_sum_resultnegative_body_terminal. fs_u_dst_append_sum_resultnegative = fs_q_dst_append_sum_resultnegative_body_terminal * S ((S (S l)) * fs_v_dst_append_sum_resultnegative) + (dst_negative_sum_append_sum_result))) /\ forall fs_i_dst_append_sum_resultnegative_body_steps. (exists fs_lt_dst_append_sum_resultnegative_body_steps_bound. fs_lt_dst_append_sum_resultnegative_body_steps_bound + S fs_i_dst_append_sum_resultnegative_body_steps = S l) -> exists fs_a_dst_append_sum_resultnegative_body_steps fs_r_dst_append_sum_resultnegative_body_steps fs_s_dst_append_sum_resultnegative_body_steps. ((((exists fs_h_dst_append_sum_resultnegative_body_steps_summand. fs_h_dst_append_sum_resultnegative_body_steps_summand + S (fs_a_dst_append_sum_resultnegative_body_steps) = S ((S (fs_i_dst_append_sum_resultnegative_body_steps)) * dst_negative_scale_append_sum_result)) /\ exists fs_q_dst_append_sum_resultnegative_body_steps_summand. dst_negative_code_append_sum_result = fs_q_dst_append_sum_resultnegative_body_steps_summand * S ((S (fs_i_dst_append_sum_resultnegative_body_steps)) * dst_negative_scale_append_sum_result) + (fs_a_dst_append_sum_resultnegative_body_steps))) /\ ((((exists fs_h_dst_append_sum_resultnegative_body_steps_partial. fs_h_dst_append_sum_resultnegative_body_steps_partial + S (fs_r_dst_append_sum_resultnegative_body_steps) = S ((S (fs_i_dst_append_sum_resultnegative_body_steps)) * fs_v_dst_append_sum_resultnegative)) /\ exists fs_q_dst_append_sum_resultnegative_body_steps_partial. fs_u_dst_append_sum_resultnegative = fs_q_dst_append_sum_resultnegative_body_steps_partial * S ((S (fs_i_dst_append_sum_resultnegative_body_steps)) * fs_v_dst_append_sum_resultnegative) + (fs_r_dst_append_sum_resultnegative_body_steps))) /\ ((((exists fs_h_dst_append_sum_resultnegative_body_steps_successor. fs_h_dst_append_sum_resultnegative_body_steps_successor + S (fs_s_dst_append_sum_resultnegative_body_steps) = S ((S (S fs_i_dst_append_sum_resultnegative_body_steps)) * fs_v_dst_append_sum_resultnegative)) /\ exists fs_q_dst_append_sum_resultnegative_body_steps_successor. fs_u_dst_append_sum_resultnegative = fs_q_dst_append_sum_resultnegative_body_steps_successor * S ((S (S fs_i_dst_append_sum_resultnegative_body_steps)) * fs_v_dst_append_sum_resultnegative) + (fs_s_dst_append_sum_resultnegative_body_steps))) /\ fs_s_dst_append_sum_resultnegative_body_steps = fs_r_dst_append_sum_resultnegative_body_steps + fs_a_dst_append_sum_resultnegative_body_steps)))))) /\ (exists ge_balance_positive_append_sum_resultresult ge_balance_negative_append_sum_resultresult. (((((c) = 2 * (ge_balance_positive_append_sum_resultresult) /\ (ge_balance_negative_append_sum_resultresult) = 0) \/ exists ge_signed_half_append_sum_resultresultdecode. (((c) = 2 * ge_signed_half_append_sum_resultresultdecode + 1 /\ (ge_balance_positive_append_sum_resultresult) = 0) /\ (ge_balance_negative_append_sum_resultresult) = S ge_signed_half_append_sum_resultresultdecode))) /\ ((dst_positive_sum_append_sum_result) + ge_balance_negative_append_sum_resultresult = (dst_negative_sum_append_sum_result) + ge_balance_positive_append_sum_resultresult)))))))))

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_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)))))))))

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
```
four_square_euler_add_swap_last · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b c. (a + b) + c = (a + c) + b
```
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_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_prefix_sum_pointwise_add · checked inherited prerequisite

Exact statement in the checked dependency cone

forall l F G H a b c. (((exists dst_positive_code_linearity_pointwiseleft_table dst_positive_scale_linearity_pointwiseleft_table dst_negative_code_linearity_pointwiseleft_table dst_negative_scale_linearity_pointwiseleft_table. (((F) = (((((dst_positive_code_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table)) * S ((dst_positive_code_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table)) + ((dst_positive_scale_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table))) + (((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) * S ((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) + ((dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)))) * S ((((dst_positive_code_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table)) * S ((dst_positive_code_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table)) + ((dst_positive_scale_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table))) + (((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) * S ((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) + ((dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)))) + ((((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) * S ((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) + ((dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table))) + (((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) * S ((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) + ((dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)))))) /\ (forall dst_index_linearity_pointwiseleft_table. (exists pvs_le_gap_linearity_pointwiseleft_tabledomain. pvs_le_gap_linearity_pointwiseleft_tabledomain + (dst_index_linearity_pointwiseleft_table) = (l)) -> exists dst_positive_linearity_pointwiseleft_table dst_negative_linearity_pointwiseleft_table dst_value_linearity_pointwiseleft_table. ((((exists ff_h_pvs_linearity_pointwiseleft_tableentrypositive. ff_h_pvs_linearity_pointwiseleft_tableentrypositive + S (dst_positive_linearity_pointwiseleft_table) = S ((S (dst_index_linearity_pointwiseleft_table)) * dst_positive_scale_linearity_pointwiseleft_table)) /\ exists ff_q_pvs_linearity_pointwiseleft_tableentrypositive. dst_positive_code_linearity_pointwiseleft_table = ff_q_pvs_linearity_pointwiseleft_tableentrypositive * S ((S (dst_index_linearity_pointwiseleft_table)) * dst_positive_scale_linearity_pointwiseleft_table) + (dst_positive_linearity_pointwiseleft_table))) /\ (((((exists ff_h_pvs_linearity_pointwiseleft_tableentrynegative. ff_h_pvs_linearity_pointwiseleft_tableentrynegative + S (dst_negative_linearity_pointwiseleft_table) = S ((S (dst_index_linearity_pointwiseleft_table)) * dst_negative_scale_linearity_pointwiseleft_table)) /\ exists ff_q_pvs_linearity_pointwiseleft_tableentrynegative. dst_negative_code_linearity_pointwiseleft_table = ff_q_pvs_linearity_pointwiseleft_tableentrynegative * S ((S (dst_index_linearity_pointwiseleft_table)) * dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_linearity_pointwiseleft_table))) /\ (exists ge_balance_positive_linearity_pointwiseleft_tableentryvalue ge_balance_negative_linearity_pointwiseleft_tableentryvalue. (((((dst_value_linearity_pointwiseleft_table) = 2 * (ge_balance_positive_linearity_pointwiseleft_tableentryvalue) /\ (ge_balance_negative_linearity_pointwiseleft_tableentryvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseleft_tableentryvaluedecode. (((dst_value_linearity_pointwiseleft_table) = 2 * ge_signed_half_linearity_pointwiseleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseleft_tableentryvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseleft_tableentryvalue) = S ge_signed_half_linearity_pointwiseleft_tableentryvaluedecode))) /\ ((dst_positive_linearity_pointwiseleft_table) + ge_balance_negative_linearity_pointwiseleft_tableentryvalue = (dst_negative_linearity_pointwiseleft_table) + ge_balance_positive_linearity_pointwiseleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_linearity_pointwiseright_table dst_positive_scale_linearity_pointwiseright_table dst_negative_code_linearity_pointwiseright_table dst_negative_scale_linearity_pointwiseright_table. (((G) = (((((dst_positive_code_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table)) * S ((dst_positive_code_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table)) + ((dst_positive_scale_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table))) + (((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) * S ((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) + ((dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)))) * S ((((dst_positive_code_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table)) * S ((dst_positive_code_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table)) + ((dst_positive_scale_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table))) + (((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) * S ((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) + ((dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)))) + ((((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) * S ((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) + ((dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table))) + (((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) * S ((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) + ((dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)))))) /\ (forall dst_index_linearity_pointwiseright_table. (exists pvs_le_gap_linearity_pointwiseright_tabledomain. pvs_le_gap_linearity_pointwiseright_tabledomain + (dst_index_linearity_pointwiseright_table) = (l)) -> exists dst_positive_linearity_pointwiseright_table dst_negative_linearity_pointwiseright_table dst_value_linearity_pointwiseright_table. ((((exists ff_h_pvs_linearity_pointwiseright_tableentrypositive. ff_h_pvs_linearity_pointwiseright_tableentrypositive + S (dst_positive_linearity_pointwiseright_table) = S ((S (dst_index_linearity_pointwiseright_table)) * dst_positive_scale_linearity_pointwiseright_table)) /\ exists ff_q_pvs_linearity_pointwiseright_tableentrypositive. dst_positive_code_linearity_pointwiseright_table = ff_q_pvs_linearity_pointwiseright_tableentrypositive * S ((S (dst_index_linearity_pointwiseright_table)) * dst_positive_scale_linearity_pointwiseright_table) + (dst_positive_linearity_pointwiseright_table))) /\ (((((exists ff_h_pvs_linearity_pointwiseright_tableentrynegative. ff_h_pvs_linearity_pointwiseright_tableentrynegative + S (dst_negative_linearity_pointwiseright_table) = S ((S (dst_index_linearity_pointwiseright_table)) * dst_negative_scale_linearity_pointwiseright_table)) /\ exists ff_q_pvs_linearity_pointwiseright_tableentrynegative. dst_negative_code_linearity_pointwiseright_table = ff_q_pvs_linearity_pointwiseright_tableentrynegative * S ((S (dst_index_linearity_pointwiseright_table)) * dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_linearity_pointwiseright_table))) /\ (exists ge_balance_positive_linearity_pointwiseright_tableentryvalue ge_balance_negative_linearity_pointwiseright_tableentryvalue. (((((dst_value_linearity_pointwiseright_table) = 2 * (ge_balance_positive_linearity_pointwiseright_tableentryvalue) /\ (ge_balance_negative_linearity_pointwiseright_tableentryvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseright_tableentryvaluedecode. (((dst_value_linearity_pointwiseright_table) = 2 * ge_signed_half_linearity_pointwiseright_tableentryvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseright_tableentryvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseright_tableentryvalue) = S ge_signed_half_linearity_pointwiseright_tableentryvaluedecode))) /\ ((dst_positive_linearity_pointwiseright_table) + ge_balance_negative_linearity_pointwiseright_tableentryvalue = (dst_negative_linearity_pointwiseright_table) + ge_balance_positive_linearity_pointwiseright_tableentryvalue))))))))) /\ (((exists dst_positive_code_linearity_pointwiseoutput_table dst_positive_scale_linearity_pointwiseoutput_table dst_negative_code_linearity_pointwiseoutput_table dst_negative_scale_linearity_pointwiseoutput_table. (((H) = (((((dst_positive_code_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table)) * S ((dst_positive_code_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table)) + ((dst_positive_scale_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table))) + (((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) * S ((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) + ((dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)))) * S ((((dst_positive_code_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table)) * S ((dst_positive_code_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table)) + ((dst_positive_scale_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table))) + (((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) * S ((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) + ((dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)))) + ((((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) * S ((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) + ((dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table))) + (((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) * S ((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) + ((dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)))))) /\ (forall dst_index_linearity_pointwiseoutput_table. (exists pvs_le_gap_linearity_pointwiseoutput_tabledomain. pvs_le_gap_linearity_pointwiseoutput_tabledomain + (dst_index_linearity_pointwiseoutput_table) = (l)) -> exists dst_positive_linearity_pointwiseoutput_table dst_negative_linearity_pointwiseoutput_table dst_value_linearity_pointwiseoutput_table. ((((exists ff_h_pvs_linearity_pointwiseoutput_tableentrypositive. ff_h_pvs_linearity_pointwiseoutput_tableentrypositive + S (dst_positive_linearity_pointwiseoutput_table) = S ((S (dst_index_linearity_pointwiseoutput_table)) * dst_positive_scale_linearity_pointwiseoutput_table)) /\ exists ff_q_pvs_linearity_pointwiseoutput_tableentrypositive. dst_positive_code_linearity_pointwiseoutput_table = ff_q_pvs_linearity_pointwiseoutput_tableentrypositive * S ((S (dst_index_linearity_pointwiseoutput_table)) * dst_positive_scale_linearity_pointwiseoutput_table) + (dst_positive_linearity_pointwiseoutput_table))) /\ (((((exists ff_h_pvs_linearity_pointwiseoutput_tableentrynegative. ff_h_pvs_linearity_pointwiseoutput_tableentrynegative + S (dst_negative_linearity_pointwiseoutput_table) = S ((S (dst_index_linearity_pointwiseoutput_table)) * dst_negative_scale_linearity_pointwiseoutput_table)) /\ exists ff_q_pvs_linearity_pointwiseoutput_tableentrynegative. dst_negative_code_linearity_pointwiseoutput_table = ff_q_pvs_linearity_pointwiseoutput_tableentrynegative * S ((S (dst_index_linearity_pointwiseoutput_table)) * dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_linearity_pointwiseoutput_table))) /\ (exists ge_balance_positive_linearity_pointwiseoutput_tableentryvalue ge_balance_negative_linearity_pointwiseoutput_tableentryvalue. (((((dst_value_linearity_pointwiseoutput_table) = 2 * (ge_balance_positive_linearity_pointwiseoutput_tableentryvalue) /\ (ge_balance_negative_linearity_pointwiseoutput_tableentryvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseoutput_tableentryvaluedecode. (((dst_value_linearity_pointwiseoutput_table) = 2 * ge_signed_half_linearity_pointwiseoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseoutput_tableentryvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseoutput_tableentryvalue) = S ge_signed_half_linearity_pointwiseoutput_tableentryvaluedecode))) /\ ((dst_positive_linearity_pointwiseoutput_table) + ge_balance_negative_linearity_pointwiseoutput_tableentryvalue = (dst_negative_linearity_pointwiseoutput_table) + ge_balance_positive_linearity_pointwiseoutput_tableentryvalue))))))))) /\ (forall sto_index_linearity_pointwiseentries. (exists pvs_gap_linearity_pointwiseentriesbound. pvs_gap_linearity_pointwiseentriesbound + S (sto_index_linearity_pointwiseentries) = (l)) -> exists sto_left_linearity_pointwiseentries sto_right_linearity_pointwiseentries sto_output_linearity_pointwiseentries. ((exists dst_positive_code_linearity_pointwiseentriesentryleft dst_positive_scale_linearity_pointwiseentriesentryleft dst_negative_code_linearity_pointwiseentriesentryleft dst_negative_scale_linearity_pointwiseentriesentryleft dst_positive_linearity_pointwiseentriesentryleft dst_negative_linearity_pointwiseentriesentryleft. (((F) = (((((dst_positive_code_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft)) * S ((dst_positive_code_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft)) + ((dst_positive_scale_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft))) + (((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) * S ((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) + ((dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)))) * S ((((dst_positive_code_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft)) * S ((dst_positive_code_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft)) + ((dst_positive_scale_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft))) + (((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) * S ((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) + ((dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)))) + ((((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) * S ((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) + ((dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft))) + (((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) * S ((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) + ((dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)))))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryleftpositive. ff_h_pvs_linearity_pointwiseentriesentryleftpositive + S (dst_positive_linearity_pointwiseentriesentryleft) = S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryleft)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryleftpositive. dst_positive_code_linearity_pointwiseentriesentryleft = ff_q_pvs_linearity_pointwiseentriesentryleftpositive * S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryleft) + (dst_positive_linearity_pointwiseentriesentryleft))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryleftnegative. ff_h_pvs_linearity_pointwiseentriesentryleftnegative + S (dst_negative_linearity_pointwiseentriesentryleft) = S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryleft)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryleftnegative. dst_negative_code_linearity_pointwiseentriesentryleft = ff_q_pvs_linearity_pointwiseentriesentryleftnegative * S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_linearity_pointwiseentriesentryleft))) /\ (exists ge_balance_positive_linearity_pointwiseentriesentryleftvalue ge_balance_negative_linearity_pointwiseentriesentryleftvalue. (((((sto_left_linearity_pointwiseentries) = 2 * (ge_balance_positive_linearity_pointwiseentriesentryleftvalue) /\ (ge_balance_negative_linearity_pointwiseentriesentryleftvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryleftvaluedecode. (((sto_left_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseentriesentryleftvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseentriesentryleftvalue) = S ge_signed_half_linearity_pointwiseentriesentryleftvaluedecode))) /\ ((dst_positive_linearity_pointwiseentriesentryleft) + ge_balance_negative_linearity_pointwiseentriesentryleftvalue = (dst_negative_linearity_pointwiseentriesentryleft) + ge_balance_positive_linearity_pointwiseentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_linearity_pointwiseentriesentryright dst_positive_scale_linearity_pointwiseentriesentryright dst_negative_code_linearity_pointwiseentriesentryright dst_negative_scale_linearity_pointwiseentriesentryright dst_positive_linearity_pointwiseentriesentryright dst_negative_linearity_pointwiseentriesentryright. (((G) = (((((dst_positive_code_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright)) * S ((dst_positive_code_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright)) + ((dst_positive_scale_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright))) + (((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) * S ((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) + ((dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)))) * S ((((dst_positive_code_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright)) * S ((dst_positive_code_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright)) + ((dst_positive_scale_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright))) + (((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) * S ((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) + ((dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)))) + ((((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) * S ((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) + ((dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright))) + (((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) * S ((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) + ((dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)))))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryrightpositive. ff_h_pvs_linearity_pointwiseentriesentryrightpositive + S (dst_positive_linearity_pointwiseentriesentryright) = S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryright)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryrightpositive. dst_positive_code_linearity_pointwiseentriesentryright = ff_q_pvs_linearity_pointwiseentriesentryrightpositive * S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryright) + (dst_positive_linearity_pointwiseentriesentryright))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryrightnegative. ff_h_pvs_linearity_pointwiseentriesentryrightnegative + S (dst_negative_linearity_pointwiseentriesentryright) = S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryright)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryrightnegative. dst_negative_code_linearity_pointwiseentriesentryright = ff_q_pvs_linearity_pointwiseentriesentryrightnegative * S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_linearity_pointwiseentriesentryright))) /\ (exists ge_balance_positive_linearity_pointwiseentriesentryrightvalue ge_balance_negative_linearity_pointwiseentriesentryrightvalue. (((((sto_right_linearity_pointwiseentries) = 2 * (ge_balance_positive_linearity_pointwiseentriesentryrightvalue) /\ (ge_balance_negative_linearity_pointwiseentriesentryrightvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryrightvaluedecode. (((sto_right_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseentriesentryrightvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseentriesentryrightvalue) = S ge_signed_half_linearity_pointwiseentriesentryrightvaluedecode))) /\ ((dst_positive_linearity_pointwiseentriesentryright) + ge_balance_negative_linearity_pointwiseentriesentryrightvalue = (dst_negative_linearity_pointwiseentriesentryright) + ge_balance_positive_linearity_pointwiseentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_linearity_pointwiseentriesentryoutput dst_positive_scale_linearity_pointwiseentriesentryoutput dst_negative_code_linearity_pointwiseentriesentryoutput dst_negative_scale_linearity_pointwiseentriesentryoutput dst_positive_linearity_pointwiseentriesentryoutput dst_negative_linearity_pointwiseentriesentryoutput. (((H) = (((((dst_positive_code_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_positive_code_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput)) + ((dst_positive_scale_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput))) + (((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) + ((dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)))) * S ((((dst_positive_code_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_positive_code_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput)) + ((dst_positive_scale_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput))) + (((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) + ((dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)))) + ((((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) + ((dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput))) + (((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) + ((dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)))))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryoutputpositive. ff_h_pvs_linearity_pointwiseentriesentryoutputpositive + S (dst_positive_linearity_pointwiseentriesentryoutput) = S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryoutput)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryoutputpositive. dst_positive_code_linearity_pointwiseentriesentryoutput = ff_q_pvs_linearity_pointwiseentriesentryoutputpositive * S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryoutput) + (dst_positive_linearity_pointwiseentriesentryoutput))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryoutputnegative. ff_h_pvs_linearity_pointwiseentriesentryoutputnegative + S (dst_negative_linearity_pointwiseentriesentryoutput) = S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryoutput)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryoutputnegative. dst_negative_code_linearity_pointwiseentriesentryoutput = ff_q_pvs_linearity_pointwiseentriesentryoutputnegative * S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_linearity_pointwiseentriesentryoutput))) /\ (exists ge_balance_positive_linearity_pointwiseentriesentryoutputvalue ge_balance_negative_linearity_pointwiseentriesentryoutputvalue. (((((sto_output_linearity_pointwiseentries) = 2 * (ge_balance_positive_linearity_pointwiseentriesentryoutputvalue) /\ (ge_balance_negative_linearity_pointwiseentriesentryoutputvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryoutputvaluedecode. (((sto_output_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseentriesentryoutputvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseentriesentryoutputvalue) = S ge_signed_half_linearity_pointwiseentriesentryoutputvaluedecode))) /\ ((dst_positive_linearity_pointwiseentriesentryoutput) + ge_balance_negative_linearity_pointwiseentriesentryoutputvalue = (dst_negative_linearity_pointwiseentriesentryoutput) + ge_balance_positive_linearity_pointwiseentriesentryoutputvalue))))))))) /\ (exists dsa_ap_linearity_pointwiseentriesentryoperation dsa_an_linearity_pointwiseentriesentryoperation dsa_bp_linearity_pointwiseentriesentryoperation dsa_bn_linearity_pointwiseentriesentryoperation dsa_cp_linearity_pointwiseentriesentryoperation dsa_cn_linearity_pointwiseentriesentryoperation. (((((sto_left_linearity_pointwiseentries) = 2 * (dsa_ap_linearity_pointwiseentriesentryoperation) /\ (dsa_an_linearity_pointwiseentriesentryoperation) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryoperationleft. (((sto_left_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryoperationleft + 1 /\ (dsa_ap_linearity_pointwiseentriesentryoperation) = 0) /\ (dsa_an_linearity_pointwiseentriesentryoperation) = S ge_signed_half_linearity_pointwiseentriesentryoperationleft))) /\ ((((((sto_right_linearity_pointwiseentries) = 2 * (dsa_bp_linearity_pointwiseentriesentryoperation) /\ (dsa_bn_linearity_pointwiseentriesentryoperation) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryoperationright. (((sto_right_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryoperationright + 1 /\ (dsa_bp_linearity_pointwiseentriesentryoperation) = 0) /\ (dsa_bn_linearity_pointwiseentriesentryoperation) = S ge_signed_half_linearity_pointwiseentriesentryoperationright))) /\ ((((((sto_output_linearity_pointwiseentries) = 2 * (dsa_cp_linearity_pointwiseentriesentryoperation) /\ (dsa_cn_linearity_pointwiseentriesentryoperation) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryoperationoutput. (((sto_output_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryoperationoutput + 1 /\ (dsa_cp_linearity_pointwiseentriesentryoperation) = 0) /\ (dsa_cn_linearity_pointwiseentriesentryoperation) = S ge_signed_half_linearity_pointwiseentriesentryoperationoutput))) /\ ((dsa_ap_linearity_pointwiseentriesentryoperation + dsa_bp_linearity_pointwiseentriesentryoperation) + dsa_cn_linearity_pointwiseentriesentryoperation = (dsa_an_linearity_pointwiseentriesentryoperation + dsa_bn_linearity_pointwiseentriesentryoperation) + dsa_cp_linearity_pointwiseentriesentryoperation))))))))))))))))))) -> (exists dst_positive_code_linearity_first dst_positive_scale_linearity_first dst_negative_code_linearity_first dst_negative_scale_linearity_first dst_positive_sum_linearity_first dst_negative_sum_linearity_first. (((F) = (((((dst_positive_code_linearity_first) + (dst_positive_scale_linearity_first)) * S ((dst_positive_code_linearity_first) + (dst_positive_scale_linearity_first)) + ((dst_positive_scale_linearity_first) + (dst_positive_scale_linearity_first))) + (((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) * S ((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) + ((dst_negative_scale_linearity_first) + (dst_negative_scale_linearity_first)))) * S ((((dst_positive_code_linearity_first) + (dst_positive_scale_linearity_first)) * S ((dst_positive_code_linearity_first) + (dst_positive_scale_linearity_first)) + ((dst_positive_scale_linearity_first) + (dst_positive_scale_linearity_first))) + (((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) * S ((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) + ((dst_negative_scale_linearity_first) + (dst_negative_scale_linearity_first)))) + ((((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) * S ((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) + ((dst_negative_scale_linearity_first) + (dst_negative_scale_linearity_first))) + (((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) * S ((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) + ((dst_negative_scale_linearity_first) + (dst_negative_scale_linearity_first)))))) /\ (((exists fs_u_dst_linearity_firstpositive fs_v_dst_linearity_firstpositive. ((((exists fs_h_dst_linearity_firstpositive_body_start. fs_h_dst_linearity_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_firstpositive)) /\ exists fs_q_dst_linearity_firstpositive_body_start. fs_u_dst_linearity_firstpositive = fs_q_dst_linearity_firstpositive_body_start * S ((S (0)) * fs_v_dst_linearity_firstpositive) + (0))) /\ ((((exists fs_h_dst_linearity_firstpositive_body_terminal. fs_h_dst_linearity_firstpositive_body_terminal + S (dst_positive_sum_linearity_first) = S ((S (l)) * fs_v_dst_linearity_firstpositive)) /\ exists fs_q_dst_linearity_firstpositive_body_terminal. fs_u_dst_linearity_firstpositive = fs_q_dst_linearity_firstpositive_body_terminal * S ((S (l)) * fs_v_dst_linearity_firstpositive) + (dst_positive_sum_linearity_first))) /\ forall fs_i_dst_linearity_firstpositive_body_steps. (exists fs_lt_dst_linearity_firstpositive_body_steps_bound. fs_lt_dst_linearity_firstpositive_body_steps_bound + S fs_i_dst_linearity_firstpositive_body_steps = l) -> exists fs_a_dst_linearity_firstpositive_body_steps fs_r_dst_linearity_firstpositive_body_steps fs_s_dst_linearity_firstpositive_body_steps. ((((exists fs_h_dst_linearity_firstpositive_body_steps_summand. fs_h_dst_linearity_firstpositive_body_steps_summand + S (fs_a_dst_linearity_firstpositive_body_steps) = S ((S (fs_i_dst_linearity_firstpositive_body_steps)) * dst_positive_scale_linearity_first)) /\ exists fs_q_dst_linearity_firstpositive_body_steps_summand. dst_positive_code_linearity_first = fs_q_dst_linearity_firstpositive_body_steps_summand * S ((S (fs_i_dst_linearity_firstpositive_body_steps)) * dst_positive_scale_linearity_first) + (fs_a_dst_linearity_firstpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_firstpositive_body_steps_partial. fs_h_dst_linearity_firstpositive_body_steps_partial + S (fs_r_dst_linearity_firstpositive_body_steps) = S ((S (fs_i_dst_linearity_firstpositive_body_steps)) * fs_v_dst_linearity_firstpositive)) /\ exists fs_q_dst_linearity_firstpositive_body_steps_partial. fs_u_dst_linearity_firstpositive = fs_q_dst_linearity_firstpositive_body_steps_partial * S ((S (fs_i_dst_linearity_firstpositive_body_steps)) * fs_v_dst_linearity_firstpositive) + (fs_r_dst_linearity_firstpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_firstpositive_body_steps_successor. fs_h_dst_linearity_firstpositive_body_steps_successor + S (fs_s_dst_linearity_firstpositive_body_steps) = S ((S (S fs_i_dst_linearity_firstpositive_body_steps)) * fs_v_dst_linearity_firstpositive)) /\ exists fs_q_dst_linearity_firstpositive_body_steps_successor. fs_u_dst_linearity_firstpositive = fs_q_dst_linearity_firstpositive_body_steps_successor * S ((S (S fs_i_dst_linearity_firstpositive_body_steps)) * fs_v_dst_linearity_firstpositive) + (fs_s_dst_linearity_firstpositive_body_steps))) /\ fs_s_dst_linearity_firstpositive_body_steps = fs_r_dst_linearity_firstpositive_body_steps + fs_a_dst_linearity_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_linearity_firstnegative fs_v_dst_linearity_firstnegative. ((((exists fs_h_dst_linearity_firstnegative_body_start. fs_h_dst_linearity_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_firstnegative)) /\ exists fs_q_dst_linearity_firstnegative_body_start. fs_u_dst_linearity_firstnegative = fs_q_dst_linearity_firstnegative_body_start * S ((S (0)) * fs_v_dst_linearity_firstnegative) + (0))) /\ ((((exists fs_h_dst_linearity_firstnegative_body_terminal. fs_h_dst_linearity_firstnegative_body_terminal + S (dst_negative_sum_linearity_first) = S ((S (l)) * fs_v_dst_linearity_firstnegative)) /\ exists fs_q_dst_linearity_firstnegative_body_terminal. fs_u_dst_linearity_firstnegative = fs_q_dst_linearity_firstnegative_body_terminal * S ((S (l)) * fs_v_dst_linearity_firstnegative) + (dst_negative_sum_linearity_first))) /\ forall fs_i_dst_linearity_firstnegative_body_steps. (exists fs_lt_dst_linearity_firstnegative_body_steps_bound. fs_lt_dst_linearity_firstnegative_body_steps_bound + S fs_i_dst_linearity_firstnegative_body_steps = l) -> exists fs_a_dst_linearity_firstnegative_body_steps fs_r_dst_linearity_firstnegative_body_steps fs_s_dst_linearity_firstnegative_body_steps. ((((exists fs_h_dst_linearity_firstnegative_body_steps_summand. fs_h_dst_linearity_firstnegative_body_steps_summand + S (fs_a_dst_linearity_firstnegative_body_steps) = S ((S (fs_i_dst_linearity_firstnegative_body_steps)) * dst_negative_scale_linearity_first)) /\ exists fs_q_dst_linearity_firstnegative_body_steps_summand. dst_negative_code_linearity_first = fs_q_dst_linearity_firstnegative_body_steps_summand * S ((S (fs_i_dst_linearity_firstnegative_body_steps)) * dst_negative_scale_linearity_first) + (fs_a_dst_linearity_firstnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_firstnegative_body_steps_partial. fs_h_dst_linearity_firstnegative_body_steps_partial + S (fs_r_dst_linearity_firstnegative_body_steps) = S ((S (fs_i_dst_linearity_firstnegative_body_steps)) * fs_v_dst_linearity_firstnegative)) /\ exists fs_q_dst_linearity_firstnegative_body_steps_partial. fs_u_dst_linearity_firstnegative = fs_q_dst_linearity_firstnegative_body_steps_partial * S ((S (fs_i_dst_linearity_firstnegative_body_steps)) * fs_v_dst_linearity_firstnegative) + (fs_r_dst_linearity_firstnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_firstnegative_body_steps_successor. fs_h_dst_linearity_firstnegative_body_steps_successor + S (fs_s_dst_linearity_firstnegative_body_steps) = S ((S (S fs_i_dst_linearity_firstnegative_body_steps)) * fs_v_dst_linearity_firstnegative)) /\ exists fs_q_dst_linearity_firstnegative_body_steps_successor. fs_u_dst_linearity_firstnegative = fs_q_dst_linearity_firstnegative_body_steps_successor * S ((S (S fs_i_dst_linearity_firstnegative_body_steps)) * fs_v_dst_linearity_firstnegative) + (fs_s_dst_linearity_firstnegative_body_steps))) /\ fs_s_dst_linearity_firstnegative_body_steps = fs_r_dst_linearity_firstnegative_body_steps + fs_a_dst_linearity_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_linearity_firstresult ge_balance_negative_linearity_firstresult. (((((a) = 2 * (ge_balance_positive_linearity_firstresult) /\ (ge_balance_negative_linearity_firstresult) = 0) \/ exists ge_signed_half_linearity_firstresultdecode. (((a) = 2 * ge_signed_half_linearity_firstresultdecode + 1 /\ (ge_balance_positive_linearity_firstresult) = 0) /\ (ge_balance_negative_linearity_firstresult) = S ge_signed_half_linearity_firstresultdecode))) /\ ((dst_positive_sum_linearity_first) + ge_balance_negative_linearity_firstresult = (dst_negative_sum_linearity_first) + ge_balance_positive_linearity_firstresult))))))))) -> (exists dst_positive_code_linearity_second dst_positive_scale_linearity_second dst_negative_code_linearity_second dst_negative_scale_linearity_second dst_positive_sum_linearity_second dst_negative_sum_linearity_second. (((G) = (((((dst_positive_code_linearity_second) + (dst_positive_scale_linearity_second)) * S ((dst_positive_code_linearity_second) + (dst_positive_scale_linearity_second)) + ((dst_positive_scale_linearity_second) + (dst_positive_scale_linearity_second))) + (((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) * S ((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) + ((dst_negative_scale_linearity_second) + (dst_negative_scale_linearity_second)))) * S ((((dst_positive_code_linearity_second) + (dst_positive_scale_linearity_second)) * S ((dst_positive_code_linearity_second) + (dst_positive_scale_linearity_second)) + ((dst_positive_scale_linearity_second) + (dst_positive_scale_linearity_second))) + (((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) * S ((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) + ((dst_negative_scale_linearity_second) + (dst_negative_scale_linearity_second)))) + ((((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) * S ((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) + ((dst_negative_scale_linearity_second) + (dst_negative_scale_linearity_second))) + (((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) * S ((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) + ((dst_negative_scale_linearity_second) + (dst_negative_scale_linearity_second)))))) /\ (((exists fs_u_dst_linearity_secondpositive fs_v_dst_linearity_secondpositive. ((((exists fs_h_dst_linearity_secondpositive_body_start. fs_h_dst_linearity_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_secondpositive)) /\ exists fs_q_dst_linearity_secondpositive_body_start. fs_u_dst_linearity_secondpositive = fs_q_dst_linearity_secondpositive_body_start * S ((S (0)) * fs_v_dst_linearity_secondpositive) + (0))) /\ ((((exists fs_h_dst_linearity_secondpositive_body_terminal. fs_h_dst_linearity_secondpositive_body_terminal + S (dst_positive_sum_linearity_second) = S ((S (l)) * fs_v_dst_linearity_secondpositive)) /\ exists fs_q_dst_linearity_secondpositive_body_terminal. fs_u_dst_linearity_secondpositive = fs_q_dst_linearity_secondpositive_body_terminal * S ((S (l)) * fs_v_dst_linearity_secondpositive) + (dst_positive_sum_linearity_second))) /\ forall fs_i_dst_linearity_secondpositive_body_steps. (exists fs_lt_dst_linearity_secondpositive_body_steps_bound. fs_lt_dst_linearity_secondpositive_body_steps_bound + S fs_i_dst_linearity_secondpositive_body_steps = l) -> exists fs_a_dst_linearity_secondpositive_body_steps fs_r_dst_linearity_secondpositive_body_steps fs_s_dst_linearity_secondpositive_body_steps. ((((exists fs_h_dst_linearity_secondpositive_body_steps_summand. fs_h_dst_linearity_secondpositive_body_steps_summand + S (fs_a_dst_linearity_secondpositive_body_steps) = S ((S (fs_i_dst_linearity_secondpositive_body_steps)) * dst_positive_scale_linearity_second)) /\ exists fs_q_dst_linearity_secondpositive_body_steps_summand. dst_positive_code_linearity_second = fs_q_dst_linearity_secondpositive_body_steps_summand * S ((S (fs_i_dst_linearity_secondpositive_body_steps)) * dst_positive_scale_linearity_second) + (fs_a_dst_linearity_secondpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_secondpositive_body_steps_partial. fs_h_dst_linearity_secondpositive_body_steps_partial + S (fs_r_dst_linearity_secondpositive_body_steps) = S ((S (fs_i_dst_linearity_secondpositive_body_steps)) * fs_v_dst_linearity_secondpositive)) /\ exists fs_q_dst_linearity_secondpositive_body_steps_partial. fs_u_dst_linearity_secondpositive = fs_q_dst_linearity_secondpositive_body_steps_partial * S ((S (fs_i_dst_linearity_secondpositive_body_steps)) * fs_v_dst_linearity_secondpositive) + (fs_r_dst_linearity_secondpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_secondpositive_body_steps_successor. fs_h_dst_linearity_secondpositive_body_steps_successor + S (fs_s_dst_linearity_secondpositive_body_steps) = S ((S (S fs_i_dst_linearity_secondpositive_body_steps)) * fs_v_dst_linearity_secondpositive)) /\ exists fs_q_dst_linearity_secondpositive_body_steps_successor. fs_u_dst_linearity_secondpositive = fs_q_dst_linearity_secondpositive_body_steps_successor * S ((S (S fs_i_dst_linearity_secondpositive_body_steps)) * fs_v_dst_linearity_secondpositive) + (fs_s_dst_linearity_secondpositive_body_steps))) /\ fs_s_dst_linearity_secondpositive_body_steps = fs_r_dst_linearity_secondpositive_body_steps + fs_a_dst_linearity_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_linearity_secondnegative fs_v_dst_linearity_secondnegative. ((((exists fs_h_dst_linearity_secondnegative_body_start. fs_h_dst_linearity_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_secondnegative)) /\ exists fs_q_dst_linearity_secondnegative_body_start. fs_u_dst_linearity_secondnegative = fs_q_dst_linearity_secondnegative_body_start * S ((S (0)) * fs_v_dst_linearity_secondnegative) + (0))) /\ ((((exists fs_h_dst_linearity_secondnegative_body_terminal. fs_h_dst_linearity_secondnegative_body_terminal + S (dst_negative_sum_linearity_second) = S ((S (l)) * fs_v_dst_linearity_secondnegative)) /\ exists fs_q_dst_linearity_secondnegative_body_terminal. fs_u_dst_linearity_secondnegative = fs_q_dst_linearity_secondnegative_body_terminal * S ((S (l)) * fs_v_dst_linearity_secondnegative) + (dst_negative_sum_linearity_second))) /\ forall fs_i_dst_linearity_secondnegative_body_steps. (exists fs_lt_dst_linearity_secondnegative_body_steps_bound. fs_lt_dst_linearity_secondnegative_body_steps_bound + S fs_i_dst_linearity_secondnegative_body_steps = l) -> exists fs_a_dst_linearity_secondnegative_body_steps fs_r_dst_linearity_secondnegative_body_steps fs_s_dst_linearity_secondnegative_body_steps. ((((exists fs_h_dst_linearity_secondnegative_body_steps_summand. fs_h_dst_linearity_secondnegative_body_steps_summand + S (fs_a_dst_linearity_secondnegative_body_steps) = S ((S (fs_i_dst_linearity_secondnegative_body_steps)) * dst_negative_scale_linearity_second)) /\ exists fs_q_dst_linearity_secondnegative_body_steps_summand. dst_negative_code_linearity_second = fs_q_dst_linearity_secondnegative_body_steps_summand * S ((S (fs_i_dst_linearity_secondnegative_body_steps)) * dst_negative_scale_linearity_second) + (fs_a_dst_linearity_secondnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_secondnegative_body_steps_partial. fs_h_dst_linearity_secondnegative_body_steps_partial + S (fs_r_dst_linearity_secondnegative_body_steps) = S ((S (fs_i_dst_linearity_secondnegative_body_steps)) * fs_v_dst_linearity_secondnegative)) /\ exists fs_q_dst_linearity_secondnegative_body_steps_partial. fs_u_dst_linearity_secondnegative = fs_q_dst_linearity_secondnegative_body_steps_partial * S ((S (fs_i_dst_linearity_secondnegative_body_steps)) * fs_v_dst_linearity_secondnegative) + (fs_r_dst_linearity_secondnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_secondnegative_body_steps_successor. fs_h_dst_linearity_secondnegative_body_steps_successor + S (fs_s_dst_linearity_secondnegative_body_steps) = S ((S (S fs_i_dst_linearity_secondnegative_body_steps)) * fs_v_dst_linearity_secondnegative)) /\ exists fs_q_dst_linearity_secondnegative_body_steps_successor. fs_u_dst_linearity_secondnegative = fs_q_dst_linearity_secondnegative_body_steps_successor * S ((S (S fs_i_dst_linearity_secondnegative_body_steps)) * fs_v_dst_linearity_secondnegative) + (fs_s_dst_linearity_secondnegative_body_steps))) /\ fs_s_dst_linearity_secondnegative_body_steps = fs_r_dst_linearity_secondnegative_body_steps + fs_a_dst_linearity_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_linearity_secondresult ge_balance_negative_linearity_secondresult. (((((b) = 2 * (ge_balance_positive_linearity_secondresult) /\ (ge_balance_negative_linearity_secondresult) = 0) \/ exists ge_signed_half_linearity_secondresultdecode. (((b) = 2 * ge_signed_half_linearity_secondresultdecode + 1 /\ (ge_balance_positive_linearity_secondresult) = 0) /\ (ge_balance_negative_linearity_secondresult) = S ge_signed_half_linearity_secondresultdecode))) /\ ((dst_positive_sum_linearity_second) + ge_balance_negative_linearity_secondresult = (dst_negative_sum_linearity_second) + ge_balance_positive_linearity_secondresult))))))))) -> (exists dst_positive_code_linearity_output dst_positive_scale_linearity_output dst_negative_code_linearity_output dst_negative_scale_linearity_output dst_positive_sum_linearity_output dst_negative_sum_linearity_output. (((H) = (((((dst_positive_code_linearity_output) + (dst_positive_scale_linearity_output)) * S ((dst_positive_code_linearity_output) + (dst_positive_scale_linearity_output)) + ((dst_positive_scale_linearity_output) + (dst_positive_scale_linearity_output))) + (((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) * S ((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) + ((dst_negative_scale_linearity_output) + (dst_negative_scale_linearity_output)))) * S ((((dst_positive_code_linearity_output) + (dst_positive_scale_linearity_output)) * S ((dst_positive_code_linearity_output) + (dst_positive_scale_linearity_output)) + ((dst_positive_scale_linearity_output) + (dst_positive_scale_linearity_output))) + (((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) * S ((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) + ((dst_negative_scale_linearity_output) + (dst_negative_scale_linearity_output)))) + ((((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) * S ((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) + ((dst_negative_scale_linearity_output) + (dst_negative_scale_linearity_output))) + (((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) * S ((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) + ((dst_negative_scale_linearity_output) + (dst_negative_scale_linearity_output)))))) /\ (((exists fs_u_dst_linearity_outputpositive fs_v_dst_linearity_outputpositive. ((((exists fs_h_dst_linearity_outputpositive_body_start. fs_h_dst_linearity_outputpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_outputpositive)) /\ exists fs_q_dst_linearity_outputpositive_body_start. fs_u_dst_linearity_outputpositive = fs_q_dst_linearity_outputpositive_body_start * S ((S (0)) * fs_v_dst_linearity_outputpositive) + (0))) /\ ((((exists fs_h_dst_linearity_outputpositive_body_terminal. fs_h_dst_linearity_outputpositive_body_terminal + S (dst_positive_sum_linearity_output) = S ((S (l)) * fs_v_dst_linearity_outputpositive)) /\ exists fs_q_dst_linearity_outputpositive_body_terminal. fs_u_dst_linearity_outputpositive = fs_q_dst_linearity_outputpositive_body_terminal * S ((S (l)) * fs_v_dst_linearity_outputpositive) + (dst_positive_sum_linearity_output))) /\ forall fs_i_dst_linearity_outputpositive_body_steps. (exists fs_lt_dst_linearity_outputpositive_body_steps_bound. fs_lt_dst_linearity_outputpositive_body_steps_bound + S fs_i_dst_linearity_outputpositive_body_steps = l) -> exists fs_a_dst_linearity_outputpositive_body_steps fs_r_dst_linearity_outputpositive_body_steps fs_s_dst_linearity_outputpositive_body_steps. ((((exists fs_h_dst_linearity_outputpositive_body_steps_summand. fs_h_dst_linearity_outputpositive_body_steps_summand + S (fs_a_dst_linearity_outputpositive_body_steps) = S ((S (fs_i_dst_linearity_outputpositive_body_steps)) * dst_positive_scale_linearity_output)) /\ exists fs_q_dst_linearity_outputpositive_body_steps_summand. dst_positive_code_linearity_output = fs_q_dst_linearity_outputpositive_body_steps_summand * S ((S (fs_i_dst_linearity_outputpositive_body_steps)) * dst_positive_scale_linearity_output) + (fs_a_dst_linearity_outputpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_outputpositive_body_steps_partial. fs_h_dst_linearity_outputpositive_body_steps_partial + S (fs_r_dst_linearity_outputpositive_body_steps) = S ((S (fs_i_dst_linearity_outputpositive_body_steps)) * fs_v_dst_linearity_outputpositive)) /\ exists fs_q_dst_linearity_outputpositive_body_steps_partial. fs_u_dst_linearity_outputpositive = fs_q_dst_linearity_outputpositive_body_steps_partial * S ((S (fs_i_dst_linearity_outputpositive_body_steps)) * fs_v_dst_linearity_outputpositive) + (fs_r_dst_linearity_outputpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_outputpositive_body_steps_successor. fs_h_dst_linearity_outputpositive_body_steps_successor + S (fs_s_dst_linearity_outputpositive_body_steps) = S ((S (S fs_i_dst_linearity_outputpositive_body_steps)) * fs_v_dst_linearity_outputpositive)) /\ exists fs_q_dst_linearity_outputpositive_body_steps_successor. fs_u_dst_linearity_outputpositive = fs_q_dst_linearity_outputpositive_body_steps_successor * S ((S (S fs_i_dst_linearity_outputpositive_body_steps)) * fs_v_dst_linearity_outputpositive) + (fs_s_dst_linearity_outputpositive_body_steps))) /\ fs_s_dst_linearity_outputpositive_body_steps = fs_r_dst_linearity_outputpositive_body_steps + fs_a_dst_linearity_outputpositive_body_steps)))))) /\ (((exists fs_u_dst_linearity_outputnegative fs_v_dst_linearity_outputnegative. ((((exists fs_h_dst_linearity_outputnegative_body_start. fs_h_dst_linearity_outputnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_outputnegative)) /\ exists fs_q_dst_linearity_outputnegative_body_start. fs_u_dst_linearity_outputnegative = fs_q_dst_linearity_outputnegative_body_start * S ((S (0)) * fs_v_dst_linearity_outputnegative) + (0))) /\ ((((exists fs_h_dst_linearity_outputnegative_body_terminal. fs_h_dst_linearity_outputnegative_body_terminal + S (dst_negative_sum_linearity_output) = S ((S (l)) * fs_v_dst_linearity_outputnegative)) /\ exists fs_q_dst_linearity_outputnegative_body_terminal. fs_u_dst_linearity_outputnegative = fs_q_dst_linearity_outputnegative_body_terminal * S ((S (l)) * fs_v_dst_linearity_outputnegative) + (dst_negative_sum_linearity_output))) /\ forall fs_i_dst_linearity_outputnegative_body_steps. (exists fs_lt_dst_linearity_outputnegative_body_steps_bound. fs_lt_dst_linearity_outputnegative_body_steps_bound + S fs_i_dst_linearity_outputnegative_body_steps = l) -> exists fs_a_dst_linearity_outputnegative_body_steps fs_r_dst_linearity_outputnegative_body_steps fs_s_dst_linearity_outputnegative_body_steps. ((((exists fs_h_dst_linearity_outputnegative_body_steps_summand. fs_h_dst_linearity_outputnegative_body_steps_summand + S (fs_a_dst_linearity_outputnegative_body_steps) = S ((S (fs_i_dst_linearity_outputnegative_body_steps)) * dst_negative_scale_linearity_output)) /\ exists fs_q_dst_linearity_outputnegative_body_steps_summand. dst_negative_code_linearity_output = fs_q_dst_linearity_outputnegative_body_steps_summand * S ((S (fs_i_dst_linearity_outputnegative_body_steps)) * dst_negative_scale_linearity_output) + (fs_a_dst_linearity_outputnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_outputnegative_body_steps_partial. fs_h_dst_linearity_outputnegative_body_steps_partial + S (fs_r_dst_linearity_outputnegative_body_steps) = S ((S (fs_i_dst_linearity_outputnegative_body_steps)) * fs_v_dst_linearity_outputnegative)) /\ exists fs_q_dst_linearity_outputnegative_body_steps_partial. fs_u_dst_linearity_outputnegative = fs_q_dst_linearity_outputnegative_body_steps_partial * S ((S (fs_i_dst_linearity_outputnegative_body_steps)) * fs_v_dst_linearity_outputnegative) + (fs_r_dst_linearity_outputnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_outputnegative_body_steps_successor. fs_h_dst_linearity_outputnegative_body_steps_successor + S (fs_s_dst_linearity_outputnegative_body_steps) = S ((S (S fs_i_dst_linearity_outputnegative_body_steps)) * fs_v_dst_linearity_outputnegative)) /\ exists fs_q_dst_linearity_outputnegative_body_steps_successor. fs_u_dst_linearity_outputnegative = fs_q_dst_linearity_outputnegative_body_steps_successor * S ((S (S fs_i_dst_linearity_outputnegative_body_steps)) * fs_v_dst_linearity_outputnegative) + (fs_s_dst_linearity_outputnegative_body_steps))) /\ fs_s_dst_linearity_outputnegative_body_steps = fs_r_dst_linearity_outputnegative_body_steps + fs_a_dst_linearity_outputnegative_body_steps)))))) /\ (exists ge_balance_positive_linearity_outputresult ge_balance_negative_linearity_outputresult. (((((c) = 2 * (ge_balance_positive_linearity_outputresult) /\ (ge_balance_negative_linearity_outputresult) = 0) \/ exists ge_signed_half_linearity_outputresultdecode. (((c) = 2 * ge_signed_half_linearity_outputresultdecode + 1 /\ (ge_balance_positive_linearity_outputresult) = 0) /\ (ge_balance_negative_linearity_outputresult) = S ge_signed_half_linearity_outputresultdecode))) /\ ((dst_positive_sum_linearity_output) + ge_balance_negative_linearity_outputresult = (dst_negative_sum_linearity_output) + ge_balance_positive_linearity_outputresult))))))))) -> (exists dsa_ap_linearity_result dsa_an_linearity_result dsa_bp_linearity_result dsa_bn_linearity_result dsa_cp_linearity_result dsa_cn_linearity_result. (((((a) = 2 * (dsa_ap_linearity_result) /\ (dsa_an_linearity_result) = 0) \/ exists ge_signed_half_linearity_resultleft. (((a) = 2 * ge_signed_half_linearity_resultleft + 1 /\ (dsa_ap_linearity_result) = 0) /\ (dsa_an_linearity_result) = S ge_signed_half_linearity_resultleft))) /\ ((((((b) = 2 * (dsa_bp_linearity_result) /\ (dsa_bn_linearity_result) = 0) \/ exists ge_signed_half_linearity_resultright. (((b) = 2 * ge_signed_half_linearity_resultright + 1 /\ (dsa_bp_linearity_result) = 0) /\ (dsa_bn_linearity_result) = S ge_signed_half_linearity_resultright))) /\ ((((((c) = 2 * (dsa_cp_linearity_result) /\ (dsa_cn_linearity_result) = 0) \/ exists ge_signed_half_linearity_resultoutput. (((c) = 2 * ge_signed_half_linearity_resultoutput + 1 /\ (dsa_cp_linearity_result) = 0) /\ (dsa_cn_linearity_result) = S ge_signed_half_linearity_resultoutput))) /\ ((dsa_ap_linearity_result + dsa_bp_linearity_result) + dsa_cn_linearity_result = (dsa_an_linearity_result + dsa_bn_linearity_result) + dsa_cp_linearity_result)))))))

signed_table_domain_resize · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N M F. (exists dst_positive_code_resize_input dst_positive_scale_resize_input dst_negative_code_resize_input dst_negative_scale_resize_input. (((F) = (((((dst_positive_code_resize_input) + (dst_positive_scale_resize_input)) * S ((dst_positive_code_resize_input) + (dst_positive_scale_resize_input)) + ((dst_positive_scale_resize_input) + (dst_positive_scale_resize_input))) + (((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) * S ((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) + ((dst_negative_scale_resize_input) + (dst_negative_scale_resize_input)))) * S ((((dst_positive_code_resize_input) + (dst_positive_scale_resize_input)) * S ((dst_positive_code_resize_input) + (dst_positive_scale_resize_input)) + ((dst_positive_scale_resize_input) + (dst_positive_scale_resize_input))) + (((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) * S ((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) + ((dst_negative_scale_resize_input) + (dst_negative_scale_resize_input)))) + ((((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) * S ((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) + ((dst_negative_scale_resize_input) + (dst_negative_scale_resize_input))) + (((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) * S ((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) + ((dst_negative_scale_resize_input) + (dst_negative_scale_resize_input)))))) /\ (forall dst_index_resize_input. (exists pvs_le_gap_resize_inputdomain. pvs_le_gap_resize_inputdomain + (dst_index_resize_input) = (N)) -> exists dst_positive_resize_input dst_negative_resize_input dst_value_resize_input. ((((exists ff_h_pvs_resize_inputentrypositive. ff_h_pvs_resize_inputentrypositive + S (dst_positive_resize_input) = S ((S (dst_index_resize_input)) * dst_positive_scale_resize_input)) /\ exists ff_q_pvs_resize_inputentrypositive. dst_positive_code_resize_input = ff_q_pvs_resize_inputentrypositive * S ((S (dst_index_resize_input)) * dst_positive_scale_resize_input) + (dst_positive_resize_input))) /\ (((((exists ff_h_pvs_resize_inputentrynegative. ff_h_pvs_resize_inputentrynegative + S (dst_negative_resize_input) = S ((S (dst_index_resize_input)) * dst_negative_scale_resize_input)) /\ exists ff_q_pvs_resize_inputentrynegative. dst_negative_code_resize_input = ff_q_pvs_resize_inputentrynegative * S ((S (dst_index_resize_input)) * dst_negative_scale_resize_input) + (dst_negative_resize_input))) /\ (exists ge_balance_positive_resize_inputentryvalue ge_balance_negative_resize_inputentryvalue. (((((dst_value_resize_input) = 2 * (ge_balance_positive_resize_inputentryvalue) /\ (ge_balance_negative_resize_inputentryvalue) = 0) \/ exists ge_signed_half_resize_inputentryvaluedecode. (((dst_value_resize_input) = 2 * ge_signed_half_resize_inputentryvaluedecode + 1 /\ (ge_balance_positive_resize_inputentryvalue) = 0) /\ (ge_balance_negative_resize_inputentryvalue) = S ge_signed_half_resize_inputentryvaluedecode))) /\ ((dst_positive_resize_input) + ge_balance_negative_resize_inputentryvalue = (dst_negative_resize_input) + ge_balance_positive_resize_inputentryvalue))))))))) -> (exists dst_positive_code_resize_output dst_positive_scale_resize_output dst_negative_code_resize_output dst_negative_scale_resize_output. (((F) = (((((dst_positive_code_resize_output) + (dst_positive_scale_resize_output)) * S ((dst_positive_code_resize_output) + (dst_positive_scale_resize_output)) + ((dst_positive_scale_resize_output) + (dst_positive_scale_resize_output))) + (((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) * S ((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) + ((dst_negative_scale_resize_output) + (dst_negative_scale_resize_output)))) * S ((((dst_positive_code_resize_output) + (dst_positive_scale_resize_output)) * S ((dst_positive_code_resize_output) + (dst_positive_scale_resize_output)) + ((dst_positive_scale_resize_output) + (dst_positive_scale_resize_output))) + (((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) * S ((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) + ((dst_negative_scale_resize_output) + (dst_negative_scale_resize_output)))) + ((((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) * S ((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) + ((dst_negative_scale_resize_output) + (dst_negative_scale_resize_output))) + (((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) * S ((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) + ((dst_negative_scale_resize_output) + (dst_negative_scale_resize_output)))))) /\ (forall dst_index_resize_output. (exists pvs_le_gap_resize_outputdomain. pvs_le_gap_resize_outputdomain + (dst_index_resize_output) = (M)) -> exists dst_positive_resize_output dst_negative_resize_output dst_value_resize_output. ((((exists ff_h_pvs_resize_outputentrypositive. ff_h_pvs_resize_outputentrypositive + S (dst_positive_resize_output) = S ((S (dst_index_resize_output)) * dst_positive_scale_resize_output)) /\ exists ff_q_pvs_resize_outputentrypositive. dst_positive_code_resize_output = ff_q_pvs_resize_outputentrypositive * S ((S (dst_index_resize_output)) * dst_positive_scale_resize_output) + (dst_positive_resize_output))) /\ (((((exists ff_h_pvs_resize_outputentrynegative. ff_h_pvs_resize_outputentrynegative + S (dst_negative_resize_output) = S ((S (dst_index_resize_output)) * dst_negative_scale_resize_output)) /\ exists ff_q_pvs_resize_outputentrynegative. dst_negative_code_resize_output = ff_q_pvs_resize_outputentrynegative * S ((S (dst_index_resize_output)) * dst_negative_scale_resize_output) + (dst_negative_resize_output))) /\ (exists ge_balance_positive_resize_outputentryvalue ge_balance_negative_resize_outputentryvalue. (((((dst_value_resize_output) = 2 * (ge_balance_positive_resize_outputentryvalue) /\ (ge_balance_negative_resize_outputentryvalue) = 0) \/ exists ge_signed_half_resize_outputentryvaluedecode. (((dst_value_resize_output) = 2 * ge_signed_half_resize_outputentryvaluedecode + 1 /\ (ge_balance_positive_resize_outputentryvalue) = 0) /\ (ge_balance_negative_resize_outputentryvalue) = S ge_signed_half_resize_outputentryvaluedecode))) /\ ((dst_positive_resize_output) + ge_balance_negative_resize_outputentryvalue = (dst_negative_resize_output) + ge_balance_positive_resize_outputentryvalue)))))))))

signed_table_lookup_any · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F i. (exists dst_positive_code_any_lookup_table dst_positive_scale_any_lookup_table dst_negative_code_any_lookup_table dst_negative_scale_any_lookup_table. (((F) = (((((dst_positive_code_any_lookup_table) + (dst_positive_scale_any_lookup_table)) * S ((dst_positive_code_any_lookup_table) + (dst_positive_scale_any_lookup_table)) + ((dst_positive_scale_any_lookup_table) + (dst_positive_scale_any_lookup_table))) + (((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) * S ((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) + ((dst_negative_scale_any_lookup_table) + (dst_negative_scale_any_lookup_table)))) * S ((((dst_positive_code_any_lookup_table) + (dst_positive_scale_any_lookup_table)) * S ((dst_positive_code_any_lookup_table) + (dst_positive_scale_any_lookup_table)) + ((dst_positive_scale_any_lookup_table) + (dst_positive_scale_any_lookup_table))) + (((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) * S ((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) + ((dst_negative_scale_any_lookup_table) + (dst_negative_scale_any_lookup_table)))) + ((((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) * S ((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) + ((dst_negative_scale_any_lookup_table) + (dst_negative_scale_any_lookup_table))) + (((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) * S ((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) + ((dst_negative_scale_any_lookup_table) + (dst_negative_scale_any_lookup_table)))))) /\ (forall dst_index_any_lookup_table. (exists pvs_le_gap_any_lookup_tabledomain. pvs_le_gap_any_lookup_tabledomain + (dst_index_any_lookup_table) = (N)) -> exists dst_positive_any_lookup_table dst_negative_any_lookup_table dst_value_any_lookup_table. ((((exists ff_h_pvs_any_lookup_tableentrypositive. ff_h_pvs_any_lookup_tableentrypositive + S (dst_positive_any_lookup_table) = S ((S (dst_index_any_lookup_table)) * dst_positive_scale_any_lookup_table)) /\ exists ff_q_pvs_any_lookup_tableentrypositive. dst_positive_code_any_lookup_table = ff_q_pvs_any_lookup_tableentrypositive * S ((S (dst_index_any_lookup_table)) * dst_positive_scale_any_lookup_table) + (dst_positive_any_lookup_table))) /\ (((((exists ff_h_pvs_any_lookup_tableentrynegative. ff_h_pvs_any_lookup_tableentrynegative + S (dst_negative_any_lookup_table) = S ((S (dst_index_any_lookup_table)) * dst_negative_scale_any_lookup_table)) /\ exists ff_q_pvs_any_lookup_tableentrynegative. dst_negative_code_any_lookup_table = ff_q_pvs_any_lookup_tableentrynegative * S ((S (dst_index_any_lookup_table)) * dst_negative_scale_any_lookup_table) + (dst_negative_any_lookup_table))) /\ (exists ge_balance_positive_any_lookup_tableentryvalue ge_balance_negative_any_lookup_tableentryvalue. (((((dst_value_any_lookup_table) = 2 * (ge_balance_positive_any_lookup_tableentryvalue) /\ (ge_balance_negative_any_lookup_tableentryvalue) = 0) \/ exists ge_signed_half_any_lookup_tableentryvaluedecode. (((dst_value_any_lookup_table) = 2 * ge_signed_half_any_lookup_tableentryvaluedecode + 1 /\ (ge_balance_positive_any_lookup_tableentryvalue) = 0) /\ (ge_balance_negative_any_lookup_tableentryvalue) = S ge_signed_half_any_lookup_tableentryvaluedecode))) /\ ((dst_positive_any_lookup_table) + ge_balance_negative_any_lookup_tableentryvalue = (dst_negative_any_lookup_table) + ge_balance_positive_any_lookup_tableentryvalue))))))))) -> exists z. (exists dst_positive_code_any_lookup_result dst_positive_scale_any_lookup_result dst_negative_code_any_lookup_result dst_negative_scale_any_lookup_result dst_positive_any_lookup_result dst_negative_any_lookup_result. (((F) = (((((dst_positive_code_any_lookup_result) + (dst_positive_scale_any_lookup_result)) * S ((dst_positive_code_any_lookup_result) + (dst_positive_scale_any_lookup_result)) + ((dst_positive_scale_any_lookup_result) + (dst_positive_scale_any_lookup_result))) + (((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) * S ((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) + ((dst_negative_scale_any_lookup_result) + (dst_negative_scale_any_lookup_result)))) * S ((((dst_positive_code_any_lookup_result) + (dst_positive_scale_any_lookup_result)) * S ((dst_positive_code_any_lookup_result) + (dst_positive_scale_any_lookup_result)) + ((dst_positive_scale_any_lookup_result) + (dst_positive_scale_any_lookup_result))) + (((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) * S ((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) + ((dst_negative_scale_any_lookup_result) + (dst_negative_scale_any_lookup_result)))) + ((((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) * S ((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) + ((dst_negative_scale_any_lookup_result) + (dst_negative_scale_any_lookup_result))) + (((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) * S ((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) + ((dst_negative_scale_any_lookup_result) + (dst_negative_scale_any_lookup_result)))))) /\ (((((exists ff_h_pvs_any_lookup_resultpositive. ff_h_pvs_any_lookup_resultpositive + S (dst_positive_any_lookup_result) = S ((S (i)) * dst_positive_scale_any_lookup_result)) /\ exists ff_q_pvs_any_lookup_resultpositive. dst_positive_code_any_lookup_result = ff_q_pvs_any_lookup_resultpositive * S ((S (i)) * dst_positive_scale_any_lookup_result) + (dst_positive_any_lookup_result))) /\ (((((exists ff_h_pvs_any_lookup_resultnegative. ff_h_pvs_any_lookup_resultnegative + S (dst_negative_any_lookup_result) = S ((S (i)) * dst_negative_scale_any_lookup_result)) /\ exists ff_q_pvs_any_lookup_resultnegative. dst_negative_code_any_lookup_result = ff_q_pvs_any_lookup_resultnegative * S ((S (i)) * dst_negative_scale_any_lookup_result) + (dst_negative_any_lookup_result))) /\ (exists ge_balance_positive_any_lookup_resultvalue ge_balance_negative_any_lookup_resultvalue. (((((z) = 2 * (ge_balance_positive_any_lookup_resultvalue) /\ (ge_balance_negative_any_lookup_resultvalue) = 0) \/ exists ge_signed_half_any_lookup_resultvaluedecode. (((z) = 2 * ge_signed_half_any_lookup_resultvaluedecode + 1 /\ (ge_balance_positive_any_lookup_resultvalue) = 0) /\ (ge_balance_negative_any_lookup_resultvalue) = S ge_signed_half_any_lookup_resultvaluedecode))) /\ ((dst_positive_any_lookup_result) + ge_balance_negative_any_lookup_resultvalue = (dst_negative_any_lookup_result) + ge_balance_positive_any_lookup_resultvalue)))))))))

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