divisor_signed_sum_from_components

Exact expanded first-order arithmetic statement

forall F pb pc nb nc l p n 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 fs_u_dst_sum_constructor_positive fs_v_dst_sum_constructor_positive. ((((exists fs_h_dst_sum_constructor_positive_body_start. fs_h_dst_sum_constructor_positive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_constructor_positive)) /\ exists fs_q_dst_sum_constructor_positive_body_start. fs_u_dst_sum_constructor_positive = fs_q_dst_sum_constructor_positive_body_start * S ((S (0)) * fs_v_dst_sum_constructor_positive) + (0))) /\ ((((exists fs_h_dst_sum_constructor_positive_body_terminal. fs_h_dst_sum_constructor_positive_body_terminal + S (p) = S ((S (l)) * fs_v_dst_sum_constructor_positive)) /\ exists fs_q_dst_sum_constructor_positive_body_terminal. fs_u_dst_sum_constructor_positive = fs_q_dst_sum_constructor_positive_body_terminal * S ((S (l)) * fs_v_dst_sum_constructor_positive) + (p))) /\ forall fs_i_dst_sum_constructor_positive_body_steps. (exists fs_lt_dst_sum_constructor_positive_body_steps_bound. fs_lt_dst_sum_constructor_positive_body_steps_bound + S fs_i_dst_sum_constructor_positive_body_steps = l) -> exists fs_a_dst_sum_constructor_positive_body_steps fs_r_dst_sum_constructor_positive_body_steps fs_s_dst_sum_constructor_positive_body_steps. ((((exists fs_h_dst_sum_constructor_positive_body_steps_summand. fs_h_dst_sum_constructor_positive_body_steps_summand + S (fs_a_dst_sum_constructor_positive_body_steps) = S ((S (fs_i_dst_sum_constructor_positive_body_steps)) * pc)) /\ exists fs_q_dst_sum_constructor_positive_body_steps_summand. pb = fs_q_dst_sum_constructor_positive_body_steps_summand * S ((S (fs_i_dst_sum_constructor_positive_body_steps)) * pc) + (fs_a_dst_sum_constructor_positive_body_steps))) /\ ((((exists fs_h_dst_sum_constructor_positive_body_steps_partial. fs_h_dst_sum_constructor_positive_body_steps_partial + S (fs_r_dst_sum_constructor_positive_body_steps) = S ((S (fs_i_dst_sum_constructor_positive_body_steps)) * fs_v_dst_sum_constructor_positive)) /\ exists fs_q_dst_sum_constructor_positive_body_steps_partial. fs_u_dst_sum_constructor_positive = fs_q_dst_sum_constructor_positive_body_steps_partial * S ((S (fs_i_dst_sum_constructor_positive_body_steps)) * fs_v_dst_sum_constructor_positive) + (fs_r_dst_sum_constructor_positive_body_steps))) /\ ((((exists fs_h_dst_sum_constructor_positive_body_steps_successor. fs_h_dst_sum_constructor_positive_body_steps_successor + S (fs_s_dst_sum_constructor_positive_body_steps) = S ((S (S fs_i_dst_sum_constructor_positive_body_steps)) * fs_v_dst_sum_constructor_positive)) /\ exists fs_q_dst_sum_constructor_positive_body_steps_successor. fs_u_dst_sum_constructor_positive = fs_q_dst_sum_constructor_positive_body_steps_successor * S ((S (S fs_i_dst_sum_constructor_positive_body_steps)) * fs_v_dst_sum_constructor_positive) + (fs_s_dst_sum_constructor_positive_body_steps))) /\ fs_s_dst_sum_constructor_positive_body_steps = fs_r_dst_sum_constructor_positive_body_steps + fs_a_dst_sum_constructor_positive_body_steps)))))) -> (exists fs_u_dst_sum_constructor_negative fs_v_dst_sum_constructor_negative. ((((exists fs_h_dst_sum_constructor_negative_body_start. fs_h_dst_sum_constructor_negative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_constructor_negative)) /\ exists fs_q_dst_sum_constructor_negative_body_start. fs_u_dst_sum_constructor_negative = fs_q_dst_sum_constructor_negative_body_start * S ((S (0)) * fs_v_dst_sum_constructor_negative) + (0))) /\ ((((exists fs_h_dst_sum_constructor_negative_body_terminal. fs_h_dst_sum_constructor_negative_body_terminal + S (n) = S ((S (l)) * fs_v_dst_sum_constructor_negative)) /\ exists fs_q_dst_sum_constructor_negative_body_terminal. fs_u_dst_sum_constructor_negative = fs_q_dst_sum_constructor_negative_body_terminal * S ((S (l)) * fs_v_dst_sum_constructor_negative) + (n))) /\ forall fs_i_dst_sum_constructor_negative_body_steps. (exists fs_lt_dst_sum_constructor_negative_body_steps_bound. fs_lt_dst_sum_constructor_negative_body_steps_bound + S fs_i_dst_sum_constructor_negative_body_steps = l) -> exists fs_a_dst_sum_constructor_negative_body_steps fs_r_dst_sum_constructor_negative_body_steps fs_s_dst_sum_constructor_negative_body_steps. ((((exists fs_h_dst_sum_constructor_negative_body_steps_summand. fs_h_dst_sum_constructor_negative_body_steps_summand + S (fs_a_dst_sum_constructor_negative_body_steps) = S ((S (fs_i_dst_sum_constructor_negative_body_steps)) * nc)) /\ exists fs_q_dst_sum_constructor_negative_body_steps_summand. nb = fs_q_dst_sum_constructor_negative_body_steps_summand * S ((S (fs_i_dst_sum_constructor_negative_body_steps)) * nc) + (fs_a_dst_sum_constructor_negative_body_steps))) /\ ((((exists fs_h_dst_sum_constructor_negative_body_steps_partial. fs_h_dst_sum_constructor_negative_body_steps_partial + S (fs_r_dst_sum_constructor_negative_body_steps) = S ((S (fs_i_dst_sum_constructor_negative_body_steps)) * fs_v_dst_sum_constructor_negative)) /\ exists fs_q_dst_sum_constructor_negative_body_steps_partial. fs_u_dst_sum_constructor_negative = fs_q_dst_sum_constructor_negative_body_steps_partial * S ((S (fs_i_dst_sum_constructor_negative_body_steps)) * fs_v_dst_sum_constructor_negative) + (fs_r_dst_sum_constructor_negative_body_steps))) /\ ((((exists fs_h_dst_sum_constructor_negative_body_steps_successor. fs_h_dst_sum_constructor_negative_body_steps_successor + S (fs_s_dst_sum_constructor_negative_body_steps) = S ((S (S fs_i_dst_sum_constructor_negative_body_steps)) * fs_v_dst_sum_constructor_negative)) /\ exists fs_q_dst_sum_constructor_negative_body_steps_successor. fs_u_dst_sum_constructor_negative = fs_q_dst_sum_constructor_negative_body_steps_successor * S ((S (S fs_i_dst_sum_constructor_negative_body_steps)) * fs_v_dst_sum_constructor_negative) + (fs_s_dst_sum_constructor_negative_body_steps))) /\ fs_s_dst_sum_constructor_negative_body_steps = fs_r_dst_sum_constructor_negative_body_steps + fs_a_dst_sum_constructor_negative_body_steps)))))) -> (exists ge_balance_positive_sum_constructor_balance ge_balance_negative_sum_constructor_balance. (((((z) = 2 * (ge_balance_positive_sum_constructor_balance) /\ (ge_balance_negative_sum_constructor_balance) = 0) \/ exists ge_signed_half_sum_constructor_balancedecode. (((z) = 2 * ge_signed_half_sum_constructor_balancedecode + 1 /\ (ge_balance_positive_sum_constructor_balance) = 0) /\ (ge_balance_negative_sum_constructor_balance) = S ge_signed_half_sum_constructor_balancedecode))) /\ ((p) + ge_balance_negative_sum_constructor_balance = (n) + ge_balance_positive_sum_constructor_balance))) -> (exists dst_positive_code_sum_constructor_result dst_positive_scale_sum_constructor_result dst_negative_code_sum_constructor_result dst_negative_scale_sum_constructor_result dst_positive_sum_sum_constructor_result dst_negative_sum_sum_constructor_result. (((F) = (((((dst_positive_code_sum_constructor_result) + (dst_positive_scale_sum_constructor_result)) * S ((dst_positive_code_sum_constructor_result) + (dst_positive_scale_sum_constructor_result)) + ((dst_positive_scale_sum_constructor_result) + (dst_positive_scale_sum_constructor_result))) + (((dst_negative_code_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)) * S ((dst_negative_code_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)) + ((dst_negative_scale_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)))) * S ((((dst_positive_code_sum_constructor_result) + (dst_positive_scale_sum_constructor_result)) * S ((dst_positive_code_sum_constructor_result) + (dst_positive_scale_sum_constructor_result)) + ((dst_positive_scale_sum_constructor_result) + (dst_positive_scale_sum_constructor_result))) + (((dst_negative_code_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)) * S ((dst_negative_code_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)) + ((dst_negative_scale_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)))) + ((((dst_negative_code_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)) * S ((dst_negative_code_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)) + ((dst_negative_scale_sum_constructor_result) + (dst_negative_scale_sum_constructor_result))) + (((dst_negative_code_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)) * S ((dst_negative_code_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)) + ((dst_negative_scale_sum_constructor_result) + (dst_negative_scale_sum_constructor_result)))))) /\ (((exists fs_u_dst_sum_constructor_resultpositive fs_v_dst_sum_constructor_resultpositive. ((((exists fs_h_dst_sum_constructor_resultpositive_body_start. fs_h_dst_sum_constructor_resultpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_constructor_resultpositive)) /\ exists fs_q_dst_sum_constructor_resultpositive_body_start. fs_u_dst_sum_constructor_resultpositive = fs_q_dst_sum_constructor_resultpositive_body_start * S ((S (0)) * fs_v_dst_sum_constructor_resultpositive) + (0))) /\ ((((exists fs_h_dst_sum_constructor_resultpositive_body_terminal. fs_h_dst_sum_constructor_resultpositive_body_terminal + S (dst_positive_sum_sum_constructor_result) = S ((S (l)) * fs_v_dst_sum_constructor_resultpositive)) /\ exists fs_q_dst_sum_constructor_resultpositive_body_terminal. fs_u_dst_sum_constructor_resultpositive = fs_q_dst_sum_constructor_resultpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_constructor_resultpositive) + (dst_positive_sum_sum_constructor_result))) /\ forall fs_i_dst_sum_constructor_resultpositive_body_steps. (exists fs_lt_dst_sum_constructor_resultpositive_body_steps_bound. fs_lt_dst_sum_constructor_resultpositive_body_steps_bound + S fs_i_dst_sum_constructor_resultpositive_body_steps = l) -> exists fs_a_dst_sum_constructor_resultpositive_body_steps fs_r_dst_sum_constructor_resultpositive_body_steps fs_s_dst_sum_constructor_resultpositive_body_steps. ((((exists fs_h_dst_sum_constructor_resultpositive_body_steps_summand. fs_h_dst_sum_constructor_resultpositive_body_steps_summand + S (fs_a_dst_sum_constructor_resultpositive_body_steps) = S ((S (fs_i_dst_sum_constructor_resultpositive_body_steps)) * dst_positive_scale_sum_constructor_result)) /\ exists fs_q_dst_sum_constructor_resultpositive_body_steps_summand. dst_positive_code_sum_constructor_result = fs_q_dst_sum_constructor_resultpositive_body_steps_summand * S ((S (fs_i_dst_sum_constructor_resultpositive_body_steps)) * dst_positive_scale_sum_constructor_result) + (fs_a_dst_sum_constructor_resultpositive_body_steps))) /\ ((((exists fs_h_dst_sum_constructor_resultpositive_body_steps_partial. fs_h_dst_sum_constructor_resultpositive_body_steps_partial + S (fs_r_dst_sum_constructor_resultpositive_body_steps) = S ((S (fs_i_dst_sum_constructor_resultpositive_body_steps)) * fs_v_dst_sum_constructor_resultpositive)) /\ exists fs_q_dst_sum_constructor_resultpositive_body_steps_partial. fs_u_dst_sum_constructor_resultpositive = fs_q_dst_sum_constructor_resultpositive_body_steps_partial * S ((S (fs_i_dst_sum_constructor_resultpositive_body_steps)) * fs_v_dst_sum_constructor_resultpositive) + (fs_r_dst_sum_constructor_resultpositive_body_steps))) /\ ((((exists fs_h_dst_sum_constructor_resultpositive_body_steps_successor. fs_h_dst_sum_constructor_resultpositive_body_steps_successor + S (fs_s_dst_sum_constructor_resultpositive_body_steps) = S ((S (S fs_i_dst_sum_constructor_resultpositive_body_steps)) * fs_v_dst_sum_constructor_resultpositive)) /\ exists fs_q_dst_sum_constructor_resultpositive_body_steps_successor. fs_u_dst_sum_constructor_resultpositive = fs_q_dst_sum_constructor_resultpositive_body_steps_successor * S ((S (S fs_i_dst_sum_constructor_resultpositive_body_steps)) * fs_v_dst_sum_constructor_resultpositive) + (fs_s_dst_sum_constructor_resultpositive_body_steps))) /\ fs_s_dst_sum_constructor_resultpositive_body_steps = fs_r_dst_sum_constructor_resultpositive_body_steps + fs_a_dst_sum_constructor_resultpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_constructor_resultnegative fs_v_dst_sum_constructor_resultnegative. ((((exists fs_h_dst_sum_constructor_resultnegative_body_start. fs_h_dst_sum_constructor_resultnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_constructor_resultnegative)) /\ exists fs_q_dst_sum_constructor_resultnegative_body_start. fs_u_dst_sum_constructor_resultnegative = fs_q_dst_sum_constructor_resultnegative_body_start * S ((S (0)) * fs_v_dst_sum_constructor_resultnegative) + (0))) /\ ((((exists fs_h_dst_sum_constructor_resultnegative_body_terminal. fs_h_dst_sum_constructor_resultnegative_body_terminal + S (dst_negative_sum_sum_constructor_result) = S ((S (l)) * fs_v_dst_sum_constructor_resultnegative)) /\ exists fs_q_dst_sum_constructor_resultnegative_body_terminal. fs_u_dst_sum_constructor_resultnegative = fs_q_dst_sum_constructor_resultnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_constructor_resultnegative) + (dst_negative_sum_sum_constructor_result))) /\ forall fs_i_dst_sum_constructor_resultnegative_body_steps. (exists fs_lt_dst_sum_constructor_resultnegative_body_steps_bound. fs_lt_dst_sum_constructor_resultnegative_body_steps_bound + S fs_i_dst_sum_constructor_resultnegative_body_steps = l) -> exists fs_a_dst_sum_constructor_resultnegative_body_steps fs_r_dst_sum_constructor_resultnegative_body_steps fs_s_dst_sum_constructor_resultnegative_body_steps. ((((exists fs_h_dst_sum_constructor_resultnegative_body_steps_summand. fs_h_dst_sum_constructor_resultnegative_body_steps_summand + S (fs_a_dst_sum_constructor_resultnegative_body_steps) = S ((S (fs_i_dst_sum_constructor_resultnegative_body_steps)) * dst_negative_scale_sum_constructor_result)) /\ exists fs_q_dst_sum_constructor_resultnegative_body_steps_summand. dst_negative_code_sum_constructor_result = fs_q_dst_sum_constructor_resultnegative_body_steps_summand * S ((S (fs_i_dst_sum_constructor_resultnegative_body_steps)) * dst_negative_scale_sum_constructor_result) + (fs_a_dst_sum_constructor_resultnegative_body_steps))) /\ ((((exists fs_h_dst_sum_constructor_resultnegative_body_steps_partial. fs_h_dst_sum_constructor_resultnegative_body_steps_partial + S (fs_r_dst_sum_constructor_resultnegative_body_steps) = S ((S (fs_i_dst_sum_constructor_resultnegative_body_steps)) * fs_v_dst_sum_constructor_resultnegative)) /\ exists fs_q_dst_sum_constructor_resultnegative_body_steps_partial. fs_u_dst_sum_constructor_resultnegative = fs_q_dst_sum_constructor_resultnegative_body_steps_partial * S ((S (fs_i_dst_sum_constructor_resultnegative_body_steps)) * fs_v_dst_sum_constructor_resultnegative) + (fs_r_dst_sum_constructor_resultnegative_body_steps))) /\ ((((exists fs_h_dst_sum_constructor_resultnegative_body_steps_successor. fs_h_dst_sum_constructor_resultnegative_body_steps_successor + S (fs_s_dst_sum_constructor_resultnegative_body_steps) = S ((S (S fs_i_dst_sum_constructor_resultnegative_body_steps)) * fs_v_dst_sum_constructor_resultnegative)) /\ exists fs_q_dst_sum_constructor_resultnegative_body_steps_successor. fs_u_dst_sum_constructor_resultnegative = fs_q_dst_sum_constructor_resultnegative_body_steps_successor * S ((S (S fs_i_dst_sum_constructor_resultnegative_body_steps)) * fs_v_dst_sum_constructor_resultnegative) + (fs_s_dst_sum_constructor_resultnegative_body_steps))) /\ fs_s_dst_sum_constructor_resultnegative_body_steps = fs_r_dst_sum_constructor_resultnegative_body_steps + fs_a_dst_sum_constructor_resultnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_constructor_resultresult ge_balance_negative_sum_constructor_resultresult. (((((z) = 2 * (ge_balance_positive_sum_constructor_resultresult) /\ (ge_balance_negative_sum_constructor_resultresult) = 0) \/ exists ge_signed_half_sum_constructor_resultresultdecode. (((z) = 2 * ge_signed_half_sum_constructor_resultresultdecode + 1 /\ (ge_balance_positive_sum_constructor_resultresult) = 0) /\ (ge_balance_negative_sum_constructor_resultresult) = S ge_signed_half_sum_constructor_resultresultdecode))) /\ ((dst_positive_sum_sum_constructor_result) + ge_balance_negative_sum_constructor_resultresult = (dst_negative_sum_sum_constructor_result) + ge_balance_positive_sum_constructor_resultresult)))))))))