Actual signed finite support — 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.

170 checked bundle nodes · 397 proof edges · 8697 body proof nodes.

Literal self-contained proof bundle · SHA-256 99d889c64fb066f79247afa4310e0143f42bfffbc2cf56e4bd9be3735e0cac47

signed_finite_support_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

ZS0001 signed_zero_window_empty · actual bundle node 161
ZS0002 signed_zero_window_restrict · actual bundle node 162
ZS0003 signed_zero_window_raise_lower · actual bundle node 163
ZS0004 signed_prefix_sum_zero_tail · actual bundle node 164
ZS0005 signed_prefix_sum_zero_value · actual bundle node 165
ZS0006 signed_prefix_sum_zero_exists · actual bundle node 166
ZS0007 signed_prefix_sum_last_value · actual bundle node 167
ZS0008 signed_prefix_sum_zero_padding_iff · actual bundle node 168

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

divisor_signed_sum_empty_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall 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_empty_result dst_positive_scale_empty_result dst_negative_code_empty_result dst_negative_scale_empty_result dst_positive_sum_empty_result dst_negative_sum_empty_result. (((F) = (((((dst_positive_code_empty_result) + (dst_positive_scale_empty_result)) * S ((dst_positive_code_empty_result) + (dst_positive_scale_empty_result)) + ((dst_positive_scale_empty_result) + (dst_positive_scale_empty_result))) + (((dst_negative_code_empty_result) + (dst_negative_scale_empty_result)) * S ((dst_negative_code_empty_result) + (dst_negative_scale_empty_result)) + ((dst_negative_scale_empty_result) + (dst_negative_scale_empty_result)))) * S ((((dst_positive_code_empty_result) + (dst_positive_scale_empty_result)) * S ((dst_positive_code_empty_result) + (dst_positive_scale_empty_result)) + ((dst_positive_scale_empty_result) + (dst_positive_scale_empty_result))) + (((dst_negative_code_empty_result) + (dst_negative_scale_empty_result)) * S ((dst_negative_code_empty_result) + (dst_negative_scale_empty_result)) + ((dst_negative_scale_empty_result) + (dst_negative_scale_empty_result)))) + ((((dst_negative_code_empty_result) + (dst_negative_scale_empty_result)) * S ((dst_negative_code_empty_result) + (dst_negative_scale_empty_result)) + ((dst_negative_scale_empty_result) + (dst_negative_scale_empty_result))) + (((dst_negative_code_empty_result) + (dst_negative_scale_empty_result)) * S ((dst_negative_code_empty_result) + (dst_negative_scale_empty_result)) + ((dst_negative_scale_empty_result) + (dst_negative_scale_empty_result)))))) /\ (((exists fs_u_dst_empty_resultpositive fs_v_dst_empty_resultpositive. ((((exists fs_h_dst_empty_resultpositive_body_start. fs_h_dst_empty_resultpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_empty_resultpositive)) /\ exists fs_q_dst_empty_resultpositive_body_start. fs_u_dst_empty_resultpositive = fs_q_dst_empty_resultpositive_body_start * S ((S (0)) * fs_v_dst_empty_resultpositive) + (0))) /\ ((((exists fs_h_dst_empty_resultpositive_body_terminal. fs_h_dst_empty_resultpositive_body_terminal + S (dst_positive_sum_empty_result) = S ((S (0)) * fs_v_dst_empty_resultpositive)) /\ exists fs_q_dst_empty_resultpositive_body_terminal. fs_u_dst_empty_resultpositive = fs_q_dst_empty_resultpositive_body_terminal * S ((S (0)) * fs_v_dst_empty_resultpositive) + (dst_positive_sum_empty_result))) /\ forall fs_i_dst_empty_resultpositive_body_steps. (exists fs_lt_dst_empty_resultpositive_body_steps_bound. fs_lt_dst_empty_resultpositive_body_steps_bound + S fs_i_dst_empty_resultpositive_body_steps = 0) -> exists fs_a_dst_empty_resultpositive_body_steps fs_r_dst_empty_resultpositive_body_steps fs_s_dst_empty_resultpositive_body_steps. ((((exists fs_h_dst_empty_resultpositive_body_steps_summand. fs_h_dst_empty_resultpositive_body_steps_summand + S (fs_a_dst_empty_resultpositive_body_steps) = S ((S (fs_i_dst_empty_resultpositive_body_steps)) * dst_positive_scale_empty_result)) /\ exists fs_q_dst_empty_resultpositive_body_steps_summand. dst_positive_code_empty_result = fs_q_dst_empty_resultpositive_body_steps_summand * S ((S (fs_i_dst_empty_resultpositive_body_steps)) * dst_positive_scale_empty_result) + (fs_a_dst_empty_resultpositive_body_steps))) /\ ((((exists fs_h_dst_empty_resultpositive_body_steps_partial. fs_h_dst_empty_resultpositive_body_steps_partial + S (fs_r_dst_empty_resultpositive_body_steps) = S ((S (fs_i_dst_empty_resultpositive_body_steps)) * fs_v_dst_empty_resultpositive)) /\ exists fs_q_dst_empty_resultpositive_body_steps_partial. fs_u_dst_empty_resultpositive = fs_q_dst_empty_resultpositive_body_steps_partial * S ((S (fs_i_dst_empty_resultpositive_body_steps)) * fs_v_dst_empty_resultpositive) + (fs_r_dst_empty_resultpositive_body_steps))) /\ ((((exists fs_h_dst_empty_resultpositive_body_steps_successor. fs_h_dst_empty_resultpositive_body_steps_successor + S (fs_s_dst_empty_resultpositive_body_steps) = S ((S (S fs_i_dst_empty_resultpositive_body_steps)) * fs_v_dst_empty_resultpositive)) /\ exists fs_q_dst_empty_resultpositive_body_steps_successor. fs_u_dst_empty_resultpositive = fs_q_dst_empty_resultpositive_body_steps_successor * S ((S (S fs_i_dst_empty_resultpositive_body_steps)) * fs_v_dst_empty_resultpositive) + (fs_s_dst_empty_resultpositive_body_steps))) /\ fs_s_dst_empty_resultpositive_body_steps = fs_r_dst_empty_resultpositive_body_steps + fs_a_dst_empty_resultpositive_body_steps)))))) /\ (((exists fs_u_dst_empty_resultnegative fs_v_dst_empty_resultnegative. ((((exists fs_h_dst_empty_resultnegative_body_start. fs_h_dst_empty_resultnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_empty_resultnegative)) /\ exists fs_q_dst_empty_resultnegative_body_start. fs_u_dst_empty_resultnegative = fs_q_dst_empty_resultnegative_body_start * S ((S (0)) * fs_v_dst_empty_resultnegative) + (0))) /\ ((((exists fs_h_dst_empty_resultnegative_body_terminal. fs_h_dst_empty_resultnegative_body_terminal + S (dst_negative_sum_empty_result) = S ((S (0)) * fs_v_dst_empty_resultnegative)) /\ exists fs_q_dst_empty_resultnegative_body_terminal. fs_u_dst_empty_resultnegative = fs_q_dst_empty_resultnegative_body_terminal * S ((S (0)) * fs_v_dst_empty_resultnegative) + (dst_negative_sum_empty_result))) /\ forall fs_i_dst_empty_resultnegative_body_steps. (exists fs_lt_dst_empty_resultnegative_body_steps_bound. fs_lt_dst_empty_resultnegative_body_steps_bound + S fs_i_dst_empty_resultnegative_body_steps = 0) -> exists fs_a_dst_empty_resultnegative_body_steps fs_r_dst_empty_resultnegative_body_steps fs_s_dst_empty_resultnegative_body_steps. ((((exists fs_h_dst_empty_resultnegative_body_steps_summand. fs_h_dst_empty_resultnegative_body_steps_summand + S (fs_a_dst_empty_resultnegative_body_steps) = S ((S (fs_i_dst_empty_resultnegative_body_steps)) * dst_negative_scale_empty_result)) /\ exists fs_q_dst_empty_resultnegative_body_steps_summand. dst_negative_code_empty_result = fs_q_dst_empty_resultnegative_body_steps_summand * S ((S (fs_i_dst_empty_resultnegative_body_steps)) * dst_negative_scale_empty_result) + (fs_a_dst_empty_resultnegative_body_steps))) /\ ((((exists fs_h_dst_empty_resultnegative_body_steps_partial. fs_h_dst_empty_resultnegative_body_steps_partial + S (fs_r_dst_empty_resultnegative_body_steps) = S ((S (fs_i_dst_empty_resultnegative_body_steps)) * fs_v_dst_empty_resultnegative)) /\ exists fs_q_dst_empty_resultnegative_body_steps_partial. fs_u_dst_empty_resultnegative = fs_q_dst_empty_resultnegative_body_steps_partial * S ((S (fs_i_dst_empty_resultnegative_body_steps)) * fs_v_dst_empty_resultnegative) + (fs_r_dst_empty_resultnegative_body_steps))) /\ ((((exists fs_h_dst_empty_resultnegative_body_steps_successor. fs_h_dst_empty_resultnegative_body_steps_successor + S (fs_s_dst_empty_resultnegative_body_steps) = S ((S (S fs_i_dst_empty_resultnegative_body_steps)) * fs_v_dst_empty_resultnegative)) /\ exists fs_q_dst_empty_resultnegative_body_steps_successor. fs_u_dst_empty_resultnegative = fs_q_dst_empty_resultnegative_body_steps_successor * S ((S (S fs_i_dst_empty_resultnegative_body_steps)) * fs_v_dst_empty_resultnegative) + (fs_s_dst_empty_resultnegative_body_steps))) /\ fs_s_dst_empty_resultnegative_body_steps = fs_r_dst_empty_resultnegative_body_steps + fs_a_dst_empty_resultnegative_body_steps)))))) /\ (exists ge_balance_positive_empty_resultresult ge_balance_negative_empty_resultresult. (((((0) = 2 * (ge_balance_positive_empty_resultresult) /\ (ge_balance_negative_empty_resultresult) = 0) \/ exists ge_signed_half_empty_resultresultdecode. (((0) = 2 * ge_signed_half_empty_resultresultdecode + 1 /\ (ge_balance_positive_empty_resultresult) = 0) /\ (ge_balance_negative_empty_resultresult) = S ge_signed_half_empty_resultresultdecode))) /\ ((dst_positive_sum_empty_result) + ge_balance_negative_empty_resultresult = (dst_negative_sum_empty_result) + ge_balance_positive_empty_resultresult)))))))))

divisor_signed_sum_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F l a b. (exists dst_positive_code_sum_unique_first dst_positive_scale_sum_unique_first dst_negative_code_sum_unique_first dst_negative_scale_sum_unique_first dst_positive_sum_sum_unique_first dst_negative_sum_sum_unique_first. (((F) = (((((dst_positive_code_sum_unique_first) + (dst_positive_scale_sum_unique_first)) * S ((dst_positive_code_sum_unique_first) + (dst_positive_scale_sum_unique_first)) + ((dst_positive_scale_sum_unique_first) + (dst_positive_scale_sum_unique_first))) + (((dst_negative_code_sum_unique_first) + (dst_negative_scale_sum_unique_first)) * S ((dst_negative_code_sum_unique_first) + (dst_negative_scale_sum_unique_first)) + ((dst_negative_scale_sum_unique_first) + (dst_negative_scale_sum_unique_first)))) * S ((((dst_positive_code_sum_unique_first) + (dst_positive_scale_sum_unique_first)) * S ((dst_positive_code_sum_unique_first) + (dst_positive_scale_sum_unique_first)) + ((dst_positive_scale_sum_unique_first) + (dst_positive_scale_sum_unique_first))) + (((dst_negative_code_sum_unique_first) + (dst_negative_scale_sum_unique_first)) * S ((dst_negative_code_sum_unique_first) + (dst_negative_scale_sum_unique_first)) + ((dst_negative_scale_sum_unique_first) + (dst_negative_scale_sum_unique_first)))) + ((((dst_negative_code_sum_unique_first) + (dst_negative_scale_sum_unique_first)) * S ((dst_negative_code_sum_unique_first) + (dst_negative_scale_sum_unique_first)) + ((dst_negative_scale_sum_unique_first) + (dst_negative_scale_sum_unique_first))) + (((dst_negative_code_sum_unique_first) + (dst_negative_scale_sum_unique_first)) * S ((dst_negative_code_sum_unique_first) + (dst_negative_scale_sum_unique_first)) + ((dst_negative_scale_sum_unique_first) + (dst_negative_scale_sum_unique_first)))))) /\ (((exists fs_u_dst_sum_unique_firstpositive fs_v_dst_sum_unique_firstpositive. ((((exists fs_h_dst_sum_unique_firstpositive_body_start. fs_h_dst_sum_unique_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_firstpositive)) /\ exists fs_q_dst_sum_unique_firstpositive_body_start. fs_u_dst_sum_unique_firstpositive = fs_q_dst_sum_unique_firstpositive_body_start * S ((S (0)) * fs_v_dst_sum_unique_firstpositive) + (0))) /\ ((((exists fs_h_dst_sum_unique_firstpositive_body_terminal. fs_h_dst_sum_unique_firstpositive_body_terminal + S (dst_positive_sum_sum_unique_first) = S ((S (l)) * fs_v_dst_sum_unique_firstpositive)) /\ exists fs_q_dst_sum_unique_firstpositive_body_terminal. fs_u_dst_sum_unique_firstpositive = fs_q_dst_sum_unique_firstpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_unique_firstpositive) + (dst_positive_sum_sum_unique_first))) /\ forall fs_i_dst_sum_unique_firstpositive_body_steps. (exists fs_lt_dst_sum_unique_firstpositive_body_steps_bound. fs_lt_dst_sum_unique_firstpositive_body_steps_bound + S fs_i_dst_sum_unique_firstpositive_body_steps = l) -> exists fs_a_dst_sum_unique_firstpositive_body_steps fs_r_dst_sum_unique_firstpositive_body_steps fs_s_dst_sum_unique_firstpositive_body_steps. ((((exists fs_h_dst_sum_unique_firstpositive_body_steps_summand. fs_h_dst_sum_unique_firstpositive_body_steps_summand + S (fs_a_dst_sum_unique_firstpositive_body_steps) = S ((S (fs_i_dst_sum_unique_firstpositive_body_steps)) * dst_positive_scale_sum_unique_first)) /\ exists fs_q_dst_sum_unique_firstpositive_body_steps_summand. dst_positive_code_sum_unique_first = fs_q_dst_sum_unique_firstpositive_body_steps_summand * S ((S (fs_i_dst_sum_unique_firstpositive_body_steps)) * dst_positive_scale_sum_unique_first) + (fs_a_dst_sum_unique_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_firstpositive_body_steps_partial. fs_h_dst_sum_unique_firstpositive_body_steps_partial + S (fs_r_dst_sum_unique_firstpositive_body_steps) = S ((S (fs_i_dst_sum_unique_firstpositive_body_steps)) * fs_v_dst_sum_unique_firstpositive)) /\ exists fs_q_dst_sum_unique_firstpositive_body_steps_partial. fs_u_dst_sum_unique_firstpositive = fs_q_dst_sum_unique_firstpositive_body_steps_partial * S ((S (fs_i_dst_sum_unique_firstpositive_body_steps)) * fs_v_dst_sum_unique_firstpositive) + (fs_r_dst_sum_unique_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_firstpositive_body_steps_successor. fs_h_dst_sum_unique_firstpositive_body_steps_successor + S (fs_s_dst_sum_unique_firstpositive_body_steps) = S ((S (S fs_i_dst_sum_unique_firstpositive_body_steps)) * fs_v_dst_sum_unique_firstpositive)) /\ exists fs_q_dst_sum_unique_firstpositive_body_steps_successor. fs_u_dst_sum_unique_firstpositive = fs_q_dst_sum_unique_firstpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unique_firstpositive_body_steps)) * fs_v_dst_sum_unique_firstpositive) + (fs_s_dst_sum_unique_firstpositive_body_steps))) /\ fs_s_dst_sum_unique_firstpositive_body_steps = fs_r_dst_sum_unique_firstpositive_body_steps + fs_a_dst_sum_unique_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unique_firstnegative fs_v_dst_sum_unique_firstnegative. ((((exists fs_h_dst_sum_unique_firstnegative_body_start. fs_h_dst_sum_unique_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_firstnegative)) /\ exists fs_q_dst_sum_unique_firstnegative_body_start. fs_u_dst_sum_unique_firstnegative = fs_q_dst_sum_unique_firstnegative_body_start * S ((S (0)) * fs_v_dst_sum_unique_firstnegative) + (0))) /\ ((((exists fs_h_dst_sum_unique_firstnegative_body_terminal. fs_h_dst_sum_unique_firstnegative_body_terminal + S (dst_negative_sum_sum_unique_first) = S ((S (l)) * fs_v_dst_sum_unique_firstnegative)) /\ exists fs_q_dst_sum_unique_firstnegative_body_terminal. fs_u_dst_sum_unique_firstnegative = fs_q_dst_sum_unique_firstnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_unique_firstnegative) + (dst_negative_sum_sum_unique_first))) /\ forall fs_i_dst_sum_unique_firstnegative_body_steps. (exists fs_lt_dst_sum_unique_firstnegative_body_steps_bound. fs_lt_dst_sum_unique_firstnegative_body_steps_bound + S fs_i_dst_sum_unique_firstnegative_body_steps = l) -> exists fs_a_dst_sum_unique_firstnegative_body_steps fs_r_dst_sum_unique_firstnegative_body_steps fs_s_dst_sum_unique_firstnegative_body_steps. ((((exists fs_h_dst_sum_unique_firstnegative_body_steps_summand. fs_h_dst_sum_unique_firstnegative_body_steps_summand + S (fs_a_dst_sum_unique_firstnegative_body_steps) = S ((S (fs_i_dst_sum_unique_firstnegative_body_steps)) * dst_negative_scale_sum_unique_first)) /\ exists fs_q_dst_sum_unique_firstnegative_body_steps_summand. dst_negative_code_sum_unique_first = fs_q_dst_sum_unique_firstnegative_body_steps_summand * S ((S (fs_i_dst_sum_unique_firstnegative_body_steps)) * dst_negative_scale_sum_unique_first) + (fs_a_dst_sum_unique_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_firstnegative_body_steps_partial. fs_h_dst_sum_unique_firstnegative_body_steps_partial + S (fs_r_dst_sum_unique_firstnegative_body_steps) = S ((S (fs_i_dst_sum_unique_firstnegative_body_steps)) * fs_v_dst_sum_unique_firstnegative)) /\ exists fs_q_dst_sum_unique_firstnegative_body_steps_partial. fs_u_dst_sum_unique_firstnegative = fs_q_dst_sum_unique_firstnegative_body_steps_partial * S ((S (fs_i_dst_sum_unique_firstnegative_body_steps)) * fs_v_dst_sum_unique_firstnegative) + (fs_r_dst_sum_unique_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_firstnegative_body_steps_successor. fs_h_dst_sum_unique_firstnegative_body_steps_successor + S (fs_s_dst_sum_unique_firstnegative_body_steps) = S ((S (S fs_i_dst_sum_unique_firstnegative_body_steps)) * fs_v_dst_sum_unique_firstnegative)) /\ exists fs_q_dst_sum_unique_firstnegative_body_steps_successor. fs_u_dst_sum_unique_firstnegative = fs_q_dst_sum_unique_firstnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unique_firstnegative_body_steps)) * fs_v_dst_sum_unique_firstnegative) + (fs_s_dst_sum_unique_firstnegative_body_steps))) /\ fs_s_dst_sum_unique_firstnegative_body_steps = fs_r_dst_sum_unique_firstnegative_body_steps + fs_a_dst_sum_unique_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unique_firstresult ge_balance_negative_sum_unique_firstresult. (((((a) = 2 * (ge_balance_positive_sum_unique_firstresult) /\ (ge_balance_negative_sum_unique_firstresult) = 0) \/ exists ge_signed_half_sum_unique_firstresultdecode. (((a) = 2 * ge_signed_half_sum_unique_firstresultdecode + 1 /\ (ge_balance_positive_sum_unique_firstresult) = 0) /\ (ge_balance_negative_sum_unique_firstresult) = S ge_signed_half_sum_unique_firstresultdecode))) /\ ((dst_positive_sum_sum_unique_first) + ge_balance_negative_sum_unique_firstresult = (dst_negative_sum_sum_unique_first) + ge_balance_positive_sum_unique_firstresult))))))))) -> (exists dst_positive_code_sum_unique_second dst_positive_scale_sum_unique_second dst_negative_code_sum_unique_second dst_negative_scale_sum_unique_second dst_positive_sum_sum_unique_second dst_negative_sum_sum_unique_second. (((F) = (((((dst_positive_code_sum_unique_second) + (dst_positive_scale_sum_unique_second)) * S ((dst_positive_code_sum_unique_second) + (dst_positive_scale_sum_unique_second)) + ((dst_positive_scale_sum_unique_second) + (dst_positive_scale_sum_unique_second))) + (((dst_negative_code_sum_unique_second) + (dst_negative_scale_sum_unique_second)) * S ((dst_negative_code_sum_unique_second) + (dst_negative_scale_sum_unique_second)) + ((dst_negative_scale_sum_unique_second) + (dst_negative_scale_sum_unique_second)))) * S ((((dst_positive_code_sum_unique_second) + (dst_positive_scale_sum_unique_second)) * S ((dst_positive_code_sum_unique_second) + (dst_positive_scale_sum_unique_second)) + ((dst_positive_scale_sum_unique_second) + (dst_positive_scale_sum_unique_second))) + (((dst_negative_code_sum_unique_second) + (dst_negative_scale_sum_unique_second)) * S ((dst_negative_code_sum_unique_second) + (dst_negative_scale_sum_unique_second)) + ((dst_negative_scale_sum_unique_second) + (dst_negative_scale_sum_unique_second)))) + ((((dst_negative_code_sum_unique_second) + (dst_negative_scale_sum_unique_second)) * S ((dst_negative_code_sum_unique_second) + (dst_negative_scale_sum_unique_second)) + ((dst_negative_scale_sum_unique_second) + (dst_negative_scale_sum_unique_second))) + (((dst_negative_code_sum_unique_second) + (dst_negative_scale_sum_unique_second)) * S ((dst_negative_code_sum_unique_second) + (dst_negative_scale_sum_unique_second)) + ((dst_negative_scale_sum_unique_second) + (dst_negative_scale_sum_unique_second)))))) /\ (((exists fs_u_dst_sum_unique_secondpositive fs_v_dst_sum_unique_secondpositive. ((((exists fs_h_dst_sum_unique_secondpositive_body_start. fs_h_dst_sum_unique_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_secondpositive)) /\ exists fs_q_dst_sum_unique_secondpositive_body_start. fs_u_dst_sum_unique_secondpositive = fs_q_dst_sum_unique_secondpositive_body_start * S ((S (0)) * fs_v_dst_sum_unique_secondpositive) + (0))) /\ ((((exists fs_h_dst_sum_unique_secondpositive_body_terminal. fs_h_dst_sum_unique_secondpositive_body_terminal + S (dst_positive_sum_sum_unique_second) = S ((S (l)) * fs_v_dst_sum_unique_secondpositive)) /\ exists fs_q_dst_sum_unique_secondpositive_body_terminal. fs_u_dst_sum_unique_secondpositive = fs_q_dst_sum_unique_secondpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_unique_secondpositive) + (dst_positive_sum_sum_unique_second))) /\ forall fs_i_dst_sum_unique_secondpositive_body_steps. (exists fs_lt_dst_sum_unique_secondpositive_body_steps_bound. fs_lt_dst_sum_unique_secondpositive_body_steps_bound + S fs_i_dst_sum_unique_secondpositive_body_steps = l) -> exists fs_a_dst_sum_unique_secondpositive_body_steps fs_r_dst_sum_unique_secondpositive_body_steps fs_s_dst_sum_unique_secondpositive_body_steps. ((((exists fs_h_dst_sum_unique_secondpositive_body_steps_summand. fs_h_dst_sum_unique_secondpositive_body_steps_summand + S (fs_a_dst_sum_unique_secondpositive_body_steps) = S ((S (fs_i_dst_sum_unique_secondpositive_body_steps)) * dst_positive_scale_sum_unique_second)) /\ exists fs_q_dst_sum_unique_secondpositive_body_steps_summand. dst_positive_code_sum_unique_second = fs_q_dst_sum_unique_secondpositive_body_steps_summand * S ((S (fs_i_dst_sum_unique_secondpositive_body_steps)) * dst_positive_scale_sum_unique_second) + (fs_a_dst_sum_unique_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_secondpositive_body_steps_partial. fs_h_dst_sum_unique_secondpositive_body_steps_partial + S (fs_r_dst_sum_unique_secondpositive_body_steps) = S ((S (fs_i_dst_sum_unique_secondpositive_body_steps)) * fs_v_dst_sum_unique_secondpositive)) /\ exists fs_q_dst_sum_unique_secondpositive_body_steps_partial. fs_u_dst_sum_unique_secondpositive = fs_q_dst_sum_unique_secondpositive_body_steps_partial * S ((S (fs_i_dst_sum_unique_secondpositive_body_steps)) * fs_v_dst_sum_unique_secondpositive) + (fs_r_dst_sum_unique_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_secondpositive_body_steps_successor. fs_h_dst_sum_unique_secondpositive_body_steps_successor + S (fs_s_dst_sum_unique_secondpositive_body_steps) = S ((S (S fs_i_dst_sum_unique_secondpositive_body_steps)) * fs_v_dst_sum_unique_secondpositive)) /\ exists fs_q_dst_sum_unique_secondpositive_body_steps_successor. fs_u_dst_sum_unique_secondpositive = fs_q_dst_sum_unique_secondpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unique_secondpositive_body_steps)) * fs_v_dst_sum_unique_secondpositive) + (fs_s_dst_sum_unique_secondpositive_body_steps))) /\ fs_s_dst_sum_unique_secondpositive_body_steps = fs_r_dst_sum_unique_secondpositive_body_steps + fs_a_dst_sum_unique_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unique_secondnegative fs_v_dst_sum_unique_secondnegative. ((((exists fs_h_dst_sum_unique_secondnegative_body_start. fs_h_dst_sum_unique_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_secondnegative)) /\ exists fs_q_dst_sum_unique_secondnegative_body_start. fs_u_dst_sum_unique_secondnegative = fs_q_dst_sum_unique_secondnegative_body_start * S ((S (0)) * fs_v_dst_sum_unique_secondnegative) + (0))) /\ ((((exists fs_h_dst_sum_unique_secondnegative_body_terminal. fs_h_dst_sum_unique_secondnegative_body_terminal + S (dst_negative_sum_sum_unique_second) = S ((S (l)) * fs_v_dst_sum_unique_secondnegative)) /\ exists fs_q_dst_sum_unique_secondnegative_body_terminal. fs_u_dst_sum_unique_secondnegative = fs_q_dst_sum_unique_secondnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_unique_secondnegative) + (dst_negative_sum_sum_unique_second))) /\ forall fs_i_dst_sum_unique_secondnegative_body_steps. (exists fs_lt_dst_sum_unique_secondnegative_body_steps_bound. fs_lt_dst_sum_unique_secondnegative_body_steps_bound + S fs_i_dst_sum_unique_secondnegative_body_steps = l) -> exists fs_a_dst_sum_unique_secondnegative_body_steps fs_r_dst_sum_unique_secondnegative_body_steps fs_s_dst_sum_unique_secondnegative_body_steps. ((((exists fs_h_dst_sum_unique_secondnegative_body_steps_summand. fs_h_dst_sum_unique_secondnegative_body_steps_summand + S (fs_a_dst_sum_unique_secondnegative_body_steps) = S ((S (fs_i_dst_sum_unique_secondnegative_body_steps)) * dst_negative_scale_sum_unique_second)) /\ exists fs_q_dst_sum_unique_secondnegative_body_steps_summand. dst_negative_code_sum_unique_second = fs_q_dst_sum_unique_secondnegative_body_steps_summand * S ((S (fs_i_dst_sum_unique_secondnegative_body_steps)) * dst_negative_scale_sum_unique_second) + (fs_a_dst_sum_unique_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_secondnegative_body_steps_partial. fs_h_dst_sum_unique_secondnegative_body_steps_partial + S (fs_r_dst_sum_unique_secondnegative_body_steps) = S ((S (fs_i_dst_sum_unique_secondnegative_body_steps)) * fs_v_dst_sum_unique_secondnegative)) /\ exists fs_q_dst_sum_unique_secondnegative_body_steps_partial. fs_u_dst_sum_unique_secondnegative = fs_q_dst_sum_unique_secondnegative_body_steps_partial * S ((S (fs_i_dst_sum_unique_secondnegative_body_steps)) * fs_v_dst_sum_unique_secondnegative) + (fs_r_dst_sum_unique_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_secondnegative_body_steps_successor. fs_h_dst_sum_unique_secondnegative_body_steps_successor + S (fs_s_dst_sum_unique_secondnegative_body_steps) = S ((S (S fs_i_dst_sum_unique_secondnegative_body_steps)) * fs_v_dst_sum_unique_secondnegative)) /\ exists fs_q_dst_sum_unique_secondnegative_body_steps_successor. fs_u_dst_sum_unique_secondnegative = fs_q_dst_sum_unique_secondnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unique_secondnegative_body_steps)) * fs_v_dst_sum_unique_secondnegative) + (fs_s_dst_sum_unique_secondnegative_body_steps))) /\ fs_s_dst_sum_unique_secondnegative_body_steps = fs_r_dst_sum_unique_secondnegative_body_steps + fs_a_dst_sum_unique_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unique_secondresult ge_balance_negative_sum_unique_secondresult. (((((b) = 2 * (ge_balance_positive_sum_unique_secondresult) /\ (ge_balance_negative_sum_unique_secondresult) = 0) \/ exists ge_signed_half_sum_unique_secondresultdecode. (((b) = 2 * ge_signed_half_sum_unique_secondresultdecode + 1 /\ (ge_balance_positive_sum_unique_secondresult) = 0) /\ (ge_balance_negative_sum_unique_secondresult) = S ge_signed_half_sum_unique_secondresultdecode))) /\ ((dst_positive_sum_sum_unique_second) + ge_balance_negative_sum_unique_secondresult = (dst_negative_sum_sum_unique_second) + ge_balance_positive_sum_unique_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

le_eq_or_lt · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + a = b) -> a = b \/ exists k. k + S a = b
```
le_of_succ_le_succ · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + S a = S b) -> exists r. r + a = b
```
le_refl · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n <= n
```
le_succ_self · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n <= S n
```
le_trans · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m k. n <= m -> m <= k -> n <= k
```
le_zero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n <= 0 -> n = 0
```
lt_not_le · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + S a = b) -> ~ (exists k. k + b = a)
```

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_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_add_zero_right · checked inherited prerequisite

Exact statement in the checked dependency cone

forall input. (exists sa_lp_zero_right sa_ln_zero_right sa_rp_zero_right sa_rn_zero_right sa_op_zero_right sa_on_zero_right. (((input = 2 * sa_lp_zero_right /\ sa_ln_zero_right = 0) \/ exists sd_half_zero_right_left. ((input = 2 * sd_half_zero_right_left + 1 /\ sa_lp_zero_right = 0) /\ sa_ln_zero_right = S sd_half_zero_right_left)) /\ (((0 = 2 * sa_rp_zero_right /\ sa_rn_zero_right = 0) \/ exists sd_half_zero_right_right. ((0 = 2 * sd_half_zero_right_right + 1 /\ sa_rp_zero_right = 0) /\ sa_rn_zero_right = S sd_half_zero_right_right)) /\ (((input = 2 * sa_op_zero_right /\ sa_on_zero_right = 0) \/ exists sd_half_zero_right_output. ((input = 2 * sd_half_zero_right_output + 1 /\ sa_op_zero_right = 0) /\ sa_on_zero_right = S sd_half_zero_right_output)) /\ (sa_lp_zero_right + sa_rp_zero_right) + sa_on_zero_right = (sa_ln_zero_right + sa_rn_zero_right) + sa_op_zero_right))))

zero_le · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. 0 <= n
```