divisor_signed_sum_to_components

Exact expanded first-order arithmetic statement

forall F pb pc nb nc l z. ((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_sum_unpacked_input dst_positive_scale_sum_unpacked_input dst_negative_code_sum_unpacked_input dst_negative_scale_sum_unpacked_input dst_positive_sum_sum_unpacked_input dst_negative_sum_sum_unpacked_input. (((F) = (((((dst_positive_code_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input)) * S ((dst_positive_code_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input)) + ((dst_positive_scale_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input))) + (((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) * S ((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) + ((dst_negative_scale_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)))) * S ((((dst_positive_code_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input)) * S ((dst_positive_code_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input)) + ((dst_positive_scale_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input))) + (((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) * S ((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) + ((dst_negative_scale_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)))) + ((((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) * S ((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) + ((dst_negative_scale_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input))) + (((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) * S ((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) + ((dst_negative_scale_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)))))) /\ (((exists fs_u_dst_sum_unpacked_inputpositive fs_v_dst_sum_unpacked_inputpositive. ((((exists fs_h_dst_sum_unpacked_inputpositive_body_start. fs_h_dst_sum_unpacked_inputpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unpacked_inputpositive)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_start. fs_u_dst_sum_unpacked_inputpositive = fs_q_dst_sum_unpacked_inputpositive_body_start * S ((S (0)) * fs_v_dst_sum_unpacked_inputpositive) + (0))) /\ ((((exists fs_h_dst_sum_unpacked_inputpositive_body_terminal. fs_h_dst_sum_unpacked_inputpositive_body_terminal + S (dst_positive_sum_sum_unpacked_input) = S ((S (l)) * fs_v_dst_sum_unpacked_inputpositive)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_terminal. fs_u_dst_sum_unpacked_inputpositive = fs_q_dst_sum_unpacked_inputpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_unpacked_inputpositive) + (dst_positive_sum_sum_unpacked_input))) /\ forall fs_i_dst_sum_unpacked_inputpositive_body_steps. (exists fs_lt_dst_sum_unpacked_inputpositive_body_steps_bound. fs_lt_dst_sum_unpacked_inputpositive_body_steps_bound + S fs_i_dst_sum_unpacked_inputpositive_body_steps = l) -> exists fs_a_dst_sum_unpacked_inputpositive_body_steps fs_r_dst_sum_unpacked_inputpositive_body_steps fs_s_dst_sum_unpacked_inputpositive_body_steps. ((((exists fs_h_dst_sum_unpacked_inputpositive_body_steps_summand. fs_h_dst_sum_unpacked_inputpositive_body_steps_summand + S (fs_a_dst_sum_unpacked_inputpositive_body_steps) = S ((S (fs_i_dst_sum_unpacked_inputpositive_body_steps)) * dst_positive_scale_sum_unpacked_input)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_steps_summand. dst_positive_code_sum_unpacked_input = fs_q_dst_sum_unpacked_inputpositive_body_steps_summand * S ((S (fs_i_dst_sum_unpacked_inputpositive_body_steps)) * dst_positive_scale_sum_unpacked_input) + (fs_a_dst_sum_unpacked_inputpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_inputpositive_body_steps_partial. fs_h_dst_sum_unpacked_inputpositive_body_steps_partial + S (fs_r_dst_sum_unpacked_inputpositive_body_steps) = S ((S (fs_i_dst_sum_unpacked_inputpositive_body_steps)) * fs_v_dst_sum_unpacked_inputpositive)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_steps_partial. fs_u_dst_sum_unpacked_inputpositive = fs_q_dst_sum_unpacked_inputpositive_body_steps_partial * S ((S (fs_i_dst_sum_unpacked_inputpositive_body_steps)) * fs_v_dst_sum_unpacked_inputpositive) + (fs_r_dst_sum_unpacked_inputpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_inputpositive_body_steps_successor. fs_h_dst_sum_unpacked_inputpositive_body_steps_successor + S (fs_s_dst_sum_unpacked_inputpositive_body_steps) = S ((S (S fs_i_dst_sum_unpacked_inputpositive_body_steps)) * fs_v_dst_sum_unpacked_inputpositive)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_steps_successor. fs_u_dst_sum_unpacked_inputpositive = fs_q_dst_sum_unpacked_inputpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unpacked_inputpositive_body_steps)) * fs_v_dst_sum_unpacked_inputpositive) + (fs_s_dst_sum_unpacked_inputpositive_body_steps))) /\ fs_s_dst_sum_unpacked_inputpositive_body_steps = fs_r_dst_sum_unpacked_inputpositive_body_steps + fs_a_dst_sum_unpacked_inputpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unpacked_inputnegative fs_v_dst_sum_unpacked_inputnegative. ((((exists fs_h_dst_sum_unpacked_inputnegative_body_start. fs_h_dst_sum_unpacked_inputnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unpacked_inputnegative)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_start. fs_u_dst_sum_unpacked_inputnegative = fs_q_dst_sum_unpacked_inputnegative_body_start * S ((S (0)) * fs_v_dst_sum_unpacked_inputnegative) + (0))) /\ ((((exists fs_h_dst_sum_unpacked_inputnegative_body_terminal. fs_h_dst_sum_unpacked_inputnegative_body_terminal + S (dst_negative_sum_sum_unpacked_input) = S ((S (l)) * fs_v_dst_sum_unpacked_inputnegative)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_terminal. fs_u_dst_sum_unpacked_inputnegative = fs_q_dst_sum_unpacked_inputnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_unpacked_inputnegative) + (dst_negative_sum_sum_unpacked_input))) /\ forall fs_i_dst_sum_unpacked_inputnegative_body_steps. (exists fs_lt_dst_sum_unpacked_inputnegative_body_steps_bound. fs_lt_dst_sum_unpacked_inputnegative_body_steps_bound + S fs_i_dst_sum_unpacked_inputnegative_body_steps = l) -> exists fs_a_dst_sum_unpacked_inputnegative_body_steps fs_r_dst_sum_unpacked_inputnegative_body_steps fs_s_dst_sum_unpacked_inputnegative_body_steps. ((((exists fs_h_dst_sum_unpacked_inputnegative_body_steps_summand. fs_h_dst_sum_unpacked_inputnegative_body_steps_summand + S (fs_a_dst_sum_unpacked_inputnegative_body_steps) = S ((S (fs_i_dst_sum_unpacked_inputnegative_body_steps)) * dst_negative_scale_sum_unpacked_input)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_steps_summand. dst_negative_code_sum_unpacked_input = fs_q_dst_sum_unpacked_inputnegative_body_steps_summand * S ((S (fs_i_dst_sum_unpacked_inputnegative_body_steps)) * dst_negative_scale_sum_unpacked_input) + (fs_a_dst_sum_unpacked_inputnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_inputnegative_body_steps_partial. fs_h_dst_sum_unpacked_inputnegative_body_steps_partial + S (fs_r_dst_sum_unpacked_inputnegative_body_steps) = S ((S (fs_i_dst_sum_unpacked_inputnegative_body_steps)) * fs_v_dst_sum_unpacked_inputnegative)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_steps_partial. fs_u_dst_sum_unpacked_inputnegative = fs_q_dst_sum_unpacked_inputnegative_body_steps_partial * S ((S (fs_i_dst_sum_unpacked_inputnegative_body_steps)) * fs_v_dst_sum_unpacked_inputnegative) + (fs_r_dst_sum_unpacked_inputnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_inputnegative_body_steps_successor. fs_h_dst_sum_unpacked_inputnegative_body_steps_successor + S (fs_s_dst_sum_unpacked_inputnegative_body_steps) = S ((S (S fs_i_dst_sum_unpacked_inputnegative_body_steps)) * fs_v_dst_sum_unpacked_inputnegative)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_steps_successor. fs_u_dst_sum_unpacked_inputnegative = fs_q_dst_sum_unpacked_inputnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unpacked_inputnegative_body_steps)) * fs_v_dst_sum_unpacked_inputnegative) + (fs_s_dst_sum_unpacked_inputnegative_body_steps))) /\ fs_s_dst_sum_unpacked_inputnegative_body_steps = fs_r_dst_sum_unpacked_inputnegative_body_steps + fs_a_dst_sum_unpacked_inputnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unpacked_inputresult ge_balance_negative_sum_unpacked_inputresult. (((((z) = 2 * (ge_balance_positive_sum_unpacked_inputresult) /\ (ge_balance_negative_sum_unpacked_inputresult) = 0) \/ exists ge_signed_half_sum_unpacked_inputresultdecode. (((z) = 2 * ge_signed_half_sum_unpacked_inputresultdecode + 1 /\ (ge_balance_positive_sum_unpacked_inputresult) = 0) /\ (ge_balance_negative_sum_unpacked_inputresult) = S ge_signed_half_sum_unpacked_inputresultdecode))) /\ ((dst_positive_sum_sum_unpacked_input) + ge_balance_negative_sum_unpacked_inputresult = (dst_negative_sum_sum_unpacked_input) + ge_balance_positive_sum_unpacked_inputresult))))))))) -> exists p n. ((exists fs_u_dst_sum_unpacked_positive fs_v_dst_sum_unpacked_positive. ((((exists fs_h_dst_sum_unpacked_positive_body_start. fs_h_dst_sum_unpacked_positive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unpacked_positive)) /\ exists fs_q_dst_sum_unpacked_positive_body_start. fs_u_dst_sum_unpacked_positive = fs_q_dst_sum_unpacked_positive_body_start * S ((S (0)) * fs_v_dst_sum_unpacked_positive) + (0))) /\ ((((exists fs_h_dst_sum_unpacked_positive_body_terminal. fs_h_dst_sum_unpacked_positive_body_terminal + S (p) = S ((S (l)) * fs_v_dst_sum_unpacked_positive)) /\ exists fs_q_dst_sum_unpacked_positive_body_terminal. fs_u_dst_sum_unpacked_positive = fs_q_dst_sum_unpacked_positive_body_terminal * S ((S (l)) * fs_v_dst_sum_unpacked_positive) + (p))) /\ forall fs_i_dst_sum_unpacked_positive_body_steps. (exists fs_lt_dst_sum_unpacked_positive_body_steps_bound. fs_lt_dst_sum_unpacked_positive_body_steps_bound + S fs_i_dst_sum_unpacked_positive_body_steps = l) -> exists fs_a_dst_sum_unpacked_positive_body_steps fs_r_dst_sum_unpacked_positive_body_steps fs_s_dst_sum_unpacked_positive_body_steps. ((((exists fs_h_dst_sum_unpacked_positive_body_steps_summand. fs_h_dst_sum_unpacked_positive_body_steps_summand + S (fs_a_dst_sum_unpacked_positive_body_steps) = S ((S (fs_i_dst_sum_unpacked_positive_body_steps)) * pc)) /\ exists fs_q_dst_sum_unpacked_positive_body_steps_summand. pb = fs_q_dst_sum_unpacked_positive_body_steps_summand * S ((S (fs_i_dst_sum_unpacked_positive_body_steps)) * pc) + (fs_a_dst_sum_unpacked_positive_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_positive_body_steps_partial. fs_h_dst_sum_unpacked_positive_body_steps_partial + S (fs_r_dst_sum_unpacked_positive_body_steps) = S ((S (fs_i_dst_sum_unpacked_positive_body_steps)) * fs_v_dst_sum_unpacked_positive)) /\ exists fs_q_dst_sum_unpacked_positive_body_steps_partial. fs_u_dst_sum_unpacked_positive = fs_q_dst_sum_unpacked_positive_body_steps_partial * S ((S (fs_i_dst_sum_unpacked_positive_body_steps)) * fs_v_dst_sum_unpacked_positive) + (fs_r_dst_sum_unpacked_positive_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_positive_body_steps_successor. fs_h_dst_sum_unpacked_positive_body_steps_successor + S (fs_s_dst_sum_unpacked_positive_body_steps) = S ((S (S fs_i_dst_sum_unpacked_positive_body_steps)) * fs_v_dst_sum_unpacked_positive)) /\ exists fs_q_dst_sum_unpacked_positive_body_steps_successor. fs_u_dst_sum_unpacked_positive = fs_q_dst_sum_unpacked_positive_body_steps_successor * S ((S (S fs_i_dst_sum_unpacked_positive_body_steps)) * fs_v_dst_sum_unpacked_positive) + (fs_s_dst_sum_unpacked_positive_body_steps))) /\ fs_s_dst_sum_unpacked_positive_body_steps = fs_r_dst_sum_unpacked_positive_body_steps + fs_a_dst_sum_unpacked_positive_body_steps)))))) /\ (((exists fs_u_dst_sum_unpacked_negative fs_v_dst_sum_unpacked_negative. ((((exists fs_h_dst_sum_unpacked_negative_body_start. fs_h_dst_sum_unpacked_negative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unpacked_negative)) /\ exists fs_q_dst_sum_unpacked_negative_body_start. fs_u_dst_sum_unpacked_negative = fs_q_dst_sum_unpacked_negative_body_start * S ((S (0)) * fs_v_dst_sum_unpacked_negative) + (0))) /\ ((((exists fs_h_dst_sum_unpacked_negative_body_terminal. fs_h_dst_sum_unpacked_negative_body_terminal + S (n) = S ((S (l)) * fs_v_dst_sum_unpacked_negative)) /\ exists fs_q_dst_sum_unpacked_negative_body_terminal. fs_u_dst_sum_unpacked_negative = fs_q_dst_sum_unpacked_negative_body_terminal * S ((S (l)) * fs_v_dst_sum_unpacked_negative) + (n))) /\ forall fs_i_dst_sum_unpacked_negative_body_steps. (exists fs_lt_dst_sum_unpacked_negative_body_steps_bound. fs_lt_dst_sum_unpacked_negative_body_steps_bound + S fs_i_dst_sum_unpacked_negative_body_steps = l) -> exists fs_a_dst_sum_unpacked_negative_body_steps fs_r_dst_sum_unpacked_negative_body_steps fs_s_dst_sum_unpacked_negative_body_steps. ((((exists fs_h_dst_sum_unpacked_negative_body_steps_summand. fs_h_dst_sum_unpacked_negative_body_steps_summand + S (fs_a_dst_sum_unpacked_negative_body_steps) = S ((S (fs_i_dst_sum_unpacked_negative_body_steps)) * nc)) /\ exists fs_q_dst_sum_unpacked_negative_body_steps_summand. nb = fs_q_dst_sum_unpacked_negative_body_steps_summand * S ((S (fs_i_dst_sum_unpacked_negative_body_steps)) * nc) + (fs_a_dst_sum_unpacked_negative_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_negative_body_steps_partial. fs_h_dst_sum_unpacked_negative_body_steps_partial + S (fs_r_dst_sum_unpacked_negative_body_steps) = S ((S (fs_i_dst_sum_unpacked_negative_body_steps)) * fs_v_dst_sum_unpacked_negative)) /\ exists fs_q_dst_sum_unpacked_negative_body_steps_partial. fs_u_dst_sum_unpacked_negative = fs_q_dst_sum_unpacked_negative_body_steps_partial * S ((S (fs_i_dst_sum_unpacked_negative_body_steps)) * fs_v_dst_sum_unpacked_negative) + (fs_r_dst_sum_unpacked_negative_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_negative_body_steps_successor. fs_h_dst_sum_unpacked_negative_body_steps_successor + S (fs_s_dst_sum_unpacked_negative_body_steps) = S ((S (S fs_i_dst_sum_unpacked_negative_body_steps)) * fs_v_dst_sum_unpacked_negative)) /\ exists fs_q_dst_sum_unpacked_negative_body_steps_successor. fs_u_dst_sum_unpacked_negative = fs_q_dst_sum_unpacked_negative_body_steps_successor * S ((S (S fs_i_dst_sum_unpacked_negative_body_steps)) * fs_v_dst_sum_unpacked_negative) + (fs_s_dst_sum_unpacked_negative_body_steps))) /\ fs_s_dst_sum_unpacked_negative_body_steps = fs_r_dst_sum_unpacked_negative_body_steps + fs_a_dst_sum_unpacked_negative_body_steps)))))) /\ (exists ge_balance_positive_sum_unpacked_balance ge_balance_negative_sum_unpacked_balance. (((((z) = 2 * (ge_balance_positive_sum_unpacked_balance) /\ (ge_balance_negative_sum_unpacked_balance) = 0) \/ exists ge_signed_half_sum_unpacked_balancedecode. (((z) = 2 * ge_signed_half_sum_unpacked_balancedecode + 1 /\ (ge_balance_positive_sum_unpacked_balance) = 0) /\ (ge_balance_negative_sum_unpacked_balance) = S ge_signed_half_sum_unpacked_balancedecode))) /\ ((p) + ge_balance_negative_sum_unpacked_balance = (n) + ge_balance_positive_sum_unpacked_balance))))))