divisor_signed_sum_successor_decompose

Exact expanded first-order arithmetic statement

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