anti_invariant_signed_permutation_sum_zero

Exact expanded first-order arithmetic statement

forall F G r s l a b. (forall pfp_i_anti_bound. (exists pfp_gap_anti_boundindex. pfp_gap_anti_boundindex + S (pfp_i_anti_bound) = (l)) -> exists pfp_a_anti_bound. (((exists ff_h_pfp_anti_boundentry. ff_h_pfp_anti_boundentry + S (pfp_a_anti_bound) = S ((S (pfp_i_anti_bound)) * s)) /\ exists ff_q_pfp_anti_boundentry. r = ff_q_pfp_anti_boundentry * S ((S (pfp_i_anti_bound)) * s) + (pfp_a_anti_bound))) /\ (exists pfp_gap_anti_boundvalue. pfp_gap_anti_boundvalue + S (pfp_a_anti_bound) = (l))) -> (forall pfp_i_anti_injective pfp_j_anti_injective pfp_a_anti_injective. (exists pfp_gap_anti_injectivefirst. pfp_gap_anti_injectivefirst + S (pfp_i_anti_injective) = (l)) -> (exists pfp_gap_anti_injectivesecond. pfp_gap_anti_injectivesecond + S (pfp_j_anti_injective) = (l)) -> (((exists ff_h_pfp_anti_injectiveleft. ff_h_pfp_anti_injectiveleft + S (pfp_a_anti_injective) = S ((S (pfp_i_anti_injective)) * s)) /\ exists ff_q_pfp_anti_injectiveleft. r = ff_q_pfp_anti_injectiveleft * S ((S (pfp_i_anti_injective)) * s) + (pfp_a_anti_injective))) -> (((exists ff_h_pfp_anti_injectiveright. ff_h_pfp_anti_injectiveright + S (pfp_a_anti_injective) = S ((S (pfp_j_anti_injective)) * s)) /\ exists ff_q_pfp_anti_injectiveright. r = ff_q_pfp_anti_injectiveright * S ((S (pfp_j_anti_injective)) * s) + (pfp_a_anti_injective))) -> pfp_i_anti_injective = pfp_j_anti_injective) -> (forall dsr_index_anti_reindex dsr_image_anti_reindex dsr_value_anti_reindex. (exists pvs_gap_anti_reindexbound. pvs_gap_anti_reindexbound + S (dsr_index_anti_reindex) = (l)) -> (((exists ff_h_pvs_anti_reindexmap. ff_h_pvs_anti_reindexmap + S (dsr_image_anti_reindex) = S ((S (dsr_index_anti_reindex)) * s)) /\ exists ff_q_pvs_anti_reindexmap. r = ff_q_pvs_anti_reindexmap * S ((S (dsr_index_anti_reindex)) * s) + (dsr_image_anti_reindex))) -> (exists dst_positive_code_anti_reindexsource dst_positive_scale_anti_reindexsource dst_negative_code_anti_reindexsource dst_negative_scale_anti_reindexsource dst_positive_anti_reindexsource dst_negative_anti_reindexsource. (((F) = (((((dst_positive_code_anti_reindexsource) + (dst_positive_scale_anti_reindexsource)) * S ((dst_positive_code_anti_reindexsource) + (dst_positive_scale_anti_reindexsource)) + ((dst_positive_scale_anti_reindexsource) + (dst_positive_scale_anti_reindexsource))) + (((dst_negative_code_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)) * S ((dst_negative_code_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)) + ((dst_negative_scale_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)))) * S ((((dst_positive_code_anti_reindexsource) + (dst_positive_scale_anti_reindexsource)) * S ((dst_positive_code_anti_reindexsource) + (dst_positive_scale_anti_reindexsource)) + ((dst_positive_scale_anti_reindexsource) + (dst_positive_scale_anti_reindexsource))) + (((dst_negative_code_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)) * S ((dst_negative_code_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)) + ((dst_negative_scale_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)))) + ((((dst_negative_code_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)) * S ((dst_negative_code_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)) + ((dst_negative_scale_anti_reindexsource) + (dst_negative_scale_anti_reindexsource))) + (((dst_negative_code_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)) * S ((dst_negative_code_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)) + ((dst_negative_scale_anti_reindexsource) + (dst_negative_scale_anti_reindexsource)))))) /\ (((((exists ff_h_pvs_anti_reindexsourcepositive. ff_h_pvs_anti_reindexsourcepositive + S (dst_positive_anti_reindexsource) = S ((S (dsr_image_anti_reindex)) * dst_positive_scale_anti_reindexsource)) /\ exists ff_q_pvs_anti_reindexsourcepositive. dst_positive_code_anti_reindexsource = ff_q_pvs_anti_reindexsourcepositive * S ((S (dsr_image_anti_reindex)) * dst_positive_scale_anti_reindexsource) + (dst_positive_anti_reindexsource))) /\ (((((exists ff_h_pvs_anti_reindexsourcenegative. ff_h_pvs_anti_reindexsourcenegative + S (dst_negative_anti_reindexsource) = S ((S (dsr_image_anti_reindex)) * dst_negative_scale_anti_reindexsource)) /\ exists ff_q_pvs_anti_reindexsourcenegative. dst_negative_code_anti_reindexsource = ff_q_pvs_anti_reindexsourcenegative * S ((S (dsr_image_anti_reindex)) * dst_negative_scale_anti_reindexsource) + (dst_negative_anti_reindexsource))) /\ (exists ge_balance_positive_anti_reindexsourcevalue ge_balance_negative_anti_reindexsourcevalue. (((((dsr_value_anti_reindex) = 2 * (ge_balance_positive_anti_reindexsourcevalue) /\ (ge_balance_negative_anti_reindexsourcevalue) = 0) \/ exists ge_signed_half_anti_reindexsourcevaluedecode. (((dsr_value_anti_reindex) = 2 * ge_signed_half_anti_reindexsourcevaluedecode + 1 /\ (ge_balance_positive_anti_reindexsourcevalue) = 0) /\ (ge_balance_negative_anti_reindexsourcevalue) = S ge_signed_half_anti_reindexsourcevaluedecode))) /\ ((dst_positive_anti_reindexsource) + ge_balance_negative_anti_reindexsourcevalue = (dst_negative_anti_reindexsource) + ge_balance_positive_anti_reindexsourcevalue))))))))) -> (exists dst_positive_code_anti_reindextarget dst_positive_scale_anti_reindextarget dst_negative_code_anti_reindextarget dst_negative_scale_anti_reindextarget dst_positive_anti_reindextarget dst_negative_anti_reindextarget. (((G) = (((((dst_positive_code_anti_reindextarget) + (dst_positive_scale_anti_reindextarget)) * S ((dst_positive_code_anti_reindextarget) + (dst_positive_scale_anti_reindextarget)) + ((dst_positive_scale_anti_reindextarget) + (dst_positive_scale_anti_reindextarget))) + (((dst_negative_code_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)) * S ((dst_negative_code_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)) + ((dst_negative_scale_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)))) * S ((((dst_positive_code_anti_reindextarget) + (dst_positive_scale_anti_reindextarget)) * S ((dst_positive_code_anti_reindextarget) + (dst_positive_scale_anti_reindextarget)) + ((dst_positive_scale_anti_reindextarget) + (dst_positive_scale_anti_reindextarget))) + (((dst_negative_code_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)) * S ((dst_negative_code_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)) + ((dst_negative_scale_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)))) + ((((dst_negative_code_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)) * S ((dst_negative_code_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)) + ((dst_negative_scale_anti_reindextarget) + (dst_negative_scale_anti_reindextarget))) + (((dst_negative_code_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)) * S ((dst_negative_code_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)) + ((dst_negative_scale_anti_reindextarget) + (dst_negative_scale_anti_reindextarget)))))) /\ (((((exists ff_h_pvs_anti_reindextargetpositive. ff_h_pvs_anti_reindextargetpositive + S (dst_positive_anti_reindextarget) = S ((S (dsr_index_anti_reindex)) * dst_positive_scale_anti_reindextarget)) /\ exists ff_q_pvs_anti_reindextargetpositive. dst_positive_code_anti_reindextarget = ff_q_pvs_anti_reindextargetpositive * S ((S (dsr_index_anti_reindex)) * dst_positive_scale_anti_reindextarget) + (dst_positive_anti_reindextarget))) /\ (((((exists ff_h_pvs_anti_reindextargetnegative. ff_h_pvs_anti_reindextargetnegative + S (dst_negative_anti_reindextarget) = S ((S (dsr_index_anti_reindex)) * dst_negative_scale_anti_reindextarget)) /\ exists ff_q_pvs_anti_reindextargetnegative. dst_negative_code_anti_reindextarget = ff_q_pvs_anti_reindextargetnegative * S ((S (dsr_index_anti_reindex)) * dst_negative_scale_anti_reindextarget) + (dst_negative_anti_reindextarget))) /\ (exists ge_balance_positive_anti_reindextargetvalue ge_balance_negative_anti_reindextargetvalue. (((((dsr_value_anti_reindex) = 2 * (ge_balance_positive_anti_reindextargetvalue) /\ (ge_balance_negative_anti_reindextargetvalue) = 0) \/ exists ge_signed_half_anti_reindextargetvaluedecode. (((dsr_value_anti_reindex) = 2 * ge_signed_half_anti_reindextargetvaluedecode + 1 /\ (ge_balance_positive_anti_reindextargetvalue) = 0) /\ (ge_balance_negative_anti_reindextargetvalue) = S ge_signed_half_anti_reindextargetvaluedecode))) /\ ((dst_positive_anti_reindextarget) + ge_balance_negative_anti_reindextargetvalue = (dst_negative_anti_reindextarget) + ge_balance_positive_anti_reindextargetvalue)))))))))) -> (forall mdc_index_anti_opposite mdc_source_anti_opposite mdc_target_anti_opposite. (exists pvs_gap_anti_oppositebound. pvs_gap_anti_oppositebound + S (mdc_index_anti_opposite) = (l)) -> (exists dst_positive_code_anti_oppositefirst dst_positive_scale_anti_oppositefirst dst_negative_code_anti_oppositefirst dst_negative_scale_anti_oppositefirst dst_positive_anti_oppositefirst dst_negative_anti_oppositefirst. (((F) = (((((dst_positive_code_anti_oppositefirst) + (dst_positive_scale_anti_oppositefirst)) * S ((dst_positive_code_anti_oppositefirst) + (dst_positive_scale_anti_oppositefirst)) + ((dst_positive_scale_anti_oppositefirst) + (dst_positive_scale_anti_oppositefirst))) + (((dst_negative_code_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)) * S ((dst_negative_code_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)) + ((dst_negative_scale_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)))) * S ((((dst_positive_code_anti_oppositefirst) + (dst_positive_scale_anti_oppositefirst)) * S ((dst_positive_code_anti_oppositefirst) + (dst_positive_scale_anti_oppositefirst)) + ((dst_positive_scale_anti_oppositefirst) + (dst_positive_scale_anti_oppositefirst))) + (((dst_negative_code_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)) * S ((dst_negative_code_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)) + ((dst_negative_scale_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)))) + ((((dst_negative_code_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)) * S ((dst_negative_code_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)) + ((dst_negative_scale_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst))) + (((dst_negative_code_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)) * S ((dst_negative_code_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)) + ((dst_negative_scale_anti_oppositefirst) + (dst_negative_scale_anti_oppositefirst)))))) /\ (((((exists ff_h_pvs_anti_oppositefirstpositive. ff_h_pvs_anti_oppositefirstpositive + S (dst_positive_anti_oppositefirst) = S ((S (mdc_index_anti_opposite)) * dst_positive_scale_anti_oppositefirst)) /\ exists ff_q_pvs_anti_oppositefirstpositive. dst_positive_code_anti_oppositefirst = ff_q_pvs_anti_oppositefirstpositive * S ((S (mdc_index_anti_opposite)) * dst_positive_scale_anti_oppositefirst) + (dst_positive_anti_oppositefirst))) /\ (((((exists ff_h_pvs_anti_oppositefirstnegative. ff_h_pvs_anti_oppositefirstnegative + S (dst_negative_anti_oppositefirst) = S ((S (mdc_index_anti_opposite)) * dst_negative_scale_anti_oppositefirst)) /\ exists ff_q_pvs_anti_oppositefirstnegative. dst_negative_code_anti_oppositefirst = ff_q_pvs_anti_oppositefirstnegative * S ((S (mdc_index_anti_opposite)) * dst_negative_scale_anti_oppositefirst) + (dst_negative_anti_oppositefirst))) /\ (exists ge_balance_positive_anti_oppositefirstvalue ge_balance_negative_anti_oppositefirstvalue. (((((mdc_source_anti_opposite) = 2 * (ge_balance_positive_anti_oppositefirstvalue) /\ (ge_balance_negative_anti_oppositefirstvalue) = 0) \/ exists ge_signed_half_anti_oppositefirstvaluedecode. (((mdc_source_anti_opposite) = 2 * ge_signed_half_anti_oppositefirstvaluedecode + 1 /\ (ge_balance_positive_anti_oppositefirstvalue) = 0) /\ (ge_balance_negative_anti_oppositefirstvalue) = S ge_signed_half_anti_oppositefirstvaluedecode))) /\ ((dst_positive_anti_oppositefirst) + ge_balance_negative_anti_oppositefirstvalue = (dst_negative_anti_oppositefirst) + ge_balance_positive_anti_oppositefirstvalue))))))))) -> (exists dst_positive_code_anti_oppositesecond dst_positive_scale_anti_oppositesecond dst_negative_code_anti_oppositesecond dst_negative_scale_anti_oppositesecond dst_positive_anti_oppositesecond dst_negative_anti_oppositesecond. (((G) = (((((dst_positive_code_anti_oppositesecond) + (dst_positive_scale_anti_oppositesecond)) * S ((dst_positive_code_anti_oppositesecond) + (dst_positive_scale_anti_oppositesecond)) + ((dst_positive_scale_anti_oppositesecond) + (dst_positive_scale_anti_oppositesecond))) + (((dst_negative_code_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)) * S ((dst_negative_code_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)) + ((dst_negative_scale_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)))) * S ((((dst_positive_code_anti_oppositesecond) + (dst_positive_scale_anti_oppositesecond)) * S ((dst_positive_code_anti_oppositesecond) + (dst_positive_scale_anti_oppositesecond)) + ((dst_positive_scale_anti_oppositesecond) + (dst_positive_scale_anti_oppositesecond))) + (((dst_negative_code_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)) * S ((dst_negative_code_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)) + ((dst_negative_scale_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)))) + ((((dst_negative_code_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)) * S ((dst_negative_code_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)) + ((dst_negative_scale_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond))) + (((dst_negative_code_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)) * S ((dst_negative_code_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)) + ((dst_negative_scale_anti_oppositesecond) + (dst_negative_scale_anti_oppositesecond)))))) /\ (((((exists ff_h_pvs_anti_oppositesecondpositive. ff_h_pvs_anti_oppositesecondpositive + S (dst_positive_anti_oppositesecond) = S ((S (mdc_index_anti_opposite)) * dst_positive_scale_anti_oppositesecond)) /\ exists ff_q_pvs_anti_oppositesecondpositive. dst_positive_code_anti_oppositesecond = ff_q_pvs_anti_oppositesecondpositive * S ((S (mdc_index_anti_opposite)) * dst_positive_scale_anti_oppositesecond) + (dst_positive_anti_oppositesecond))) /\ (((((exists ff_h_pvs_anti_oppositesecondnegative. ff_h_pvs_anti_oppositesecondnegative + S (dst_negative_anti_oppositesecond) = S ((S (mdc_index_anti_opposite)) * dst_negative_scale_anti_oppositesecond)) /\ exists ff_q_pvs_anti_oppositesecondnegative. dst_negative_code_anti_oppositesecond = ff_q_pvs_anti_oppositesecondnegative * S ((S (mdc_index_anti_opposite)) * dst_negative_scale_anti_oppositesecond) + (dst_negative_anti_oppositesecond))) /\ (exists ge_balance_positive_anti_oppositesecondvalue ge_balance_negative_anti_oppositesecondvalue. (((((mdc_target_anti_opposite) = 2 * (ge_balance_positive_anti_oppositesecondvalue) /\ (ge_balance_negative_anti_oppositesecondvalue) = 0) \/ exists ge_signed_half_anti_oppositesecondvaluedecode. (((mdc_target_anti_opposite) = 2 * ge_signed_half_anti_oppositesecondvaluedecode + 1 /\ (ge_balance_positive_anti_oppositesecondvalue) = 0) /\ (ge_balance_negative_anti_oppositesecondvalue) = S ge_signed_half_anti_oppositesecondvaluedecode))) /\ ((dst_positive_anti_oppositesecond) + ge_balance_negative_anti_oppositesecondvalue = (dst_negative_anti_oppositesecond) + ge_balance_positive_anti_oppositesecondvalue))))))))) -> (exists mps_positive_anti_oppositenegation mps_negative_anti_oppositenegation. (((((mdc_source_anti_opposite) = 2 * (mps_positive_anti_oppositenegation) /\ (mps_negative_anti_oppositenegation) = 0) \/ exists ge_signed_half_anti_oppositenegationsource. (((mdc_source_anti_opposite) = 2 * ge_signed_half_anti_oppositenegationsource + 1 /\ (mps_positive_anti_oppositenegation) = 0) /\ (mps_negative_anti_oppositenegation) = S ge_signed_half_anti_oppositenegationsource))) /\ ((((mdc_target_anti_opposite) = 2 * (mps_negative_anti_oppositenegation) /\ (mps_positive_anti_oppositenegation) = 0) \/ exists ge_signed_half_anti_oppositenegationtarget. (((mdc_target_anti_opposite) = 2 * ge_signed_half_anti_oppositenegationtarget + 1 /\ (mps_negative_anti_oppositenegation) = 0) /\ (mps_positive_anti_oppositenegation) = S ge_signed_half_anti_oppositenegationtarget)))))) -> (exists dst_positive_code_anti_first_sum dst_positive_scale_anti_first_sum dst_negative_code_anti_first_sum dst_negative_scale_anti_first_sum dst_positive_sum_anti_first_sum dst_negative_sum_anti_first_sum. (((F) = (((((dst_positive_code_anti_first_sum) + (dst_positive_scale_anti_first_sum)) * S ((dst_positive_code_anti_first_sum) + (dst_positive_scale_anti_first_sum)) + ((dst_positive_scale_anti_first_sum) + (dst_positive_scale_anti_first_sum))) + (((dst_negative_code_anti_first_sum) + (dst_negative_scale_anti_first_sum)) * S ((dst_negative_code_anti_first_sum) + (dst_negative_scale_anti_first_sum)) + ((dst_negative_scale_anti_first_sum) + (dst_negative_scale_anti_first_sum)))) * S ((((dst_positive_code_anti_first_sum) + (dst_positive_scale_anti_first_sum)) * S ((dst_positive_code_anti_first_sum) + (dst_positive_scale_anti_first_sum)) + ((dst_positive_scale_anti_first_sum) + (dst_positive_scale_anti_first_sum))) + (((dst_negative_code_anti_first_sum) + (dst_negative_scale_anti_first_sum)) * S ((dst_negative_code_anti_first_sum) + (dst_negative_scale_anti_first_sum)) + ((dst_negative_scale_anti_first_sum) + (dst_negative_scale_anti_first_sum)))) + ((((dst_negative_code_anti_first_sum) + (dst_negative_scale_anti_first_sum)) * S ((dst_negative_code_anti_first_sum) + (dst_negative_scale_anti_first_sum)) + ((dst_negative_scale_anti_first_sum) + (dst_negative_scale_anti_first_sum))) + (((dst_negative_code_anti_first_sum) + (dst_negative_scale_anti_first_sum)) * S ((dst_negative_code_anti_first_sum) + (dst_negative_scale_anti_first_sum)) + ((dst_negative_scale_anti_first_sum) + (dst_negative_scale_anti_first_sum)))))) /\ (((exists fs_u_dst_anti_first_sumpositive fs_v_dst_anti_first_sumpositive. ((((exists fs_h_dst_anti_first_sumpositive_body_start. fs_h_dst_anti_first_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_anti_first_sumpositive)) /\ exists fs_q_dst_anti_first_sumpositive_body_start. fs_u_dst_anti_first_sumpositive = fs_q_dst_anti_first_sumpositive_body_start * S ((S (0)) * fs_v_dst_anti_first_sumpositive) + (0))) /\ ((((exists fs_h_dst_anti_first_sumpositive_body_terminal. fs_h_dst_anti_first_sumpositive_body_terminal + S (dst_positive_sum_anti_first_sum) = S ((S (l)) * fs_v_dst_anti_first_sumpositive)) /\ exists fs_q_dst_anti_first_sumpositive_body_terminal. fs_u_dst_anti_first_sumpositive = fs_q_dst_anti_first_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_anti_first_sumpositive) + (dst_positive_sum_anti_first_sum))) /\ forall fs_i_dst_anti_first_sumpositive_body_steps. (exists fs_lt_dst_anti_first_sumpositive_body_steps_bound. fs_lt_dst_anti_first_sumpositive_body_steps_bound + S fs_i_dst_anti_first_sumpositive_body_steps = l) -> exists fs_a_dst_anti_first_sumpositive_body_steps fs_r_dst_anti_first_sumpositive_body_steps fs_s_dst_anti_first_sumpositive_body_steps. ((((exists fs_h_dst_anti_first_sumpositive_body_steps_summand. fs_h_dst_anti_first_sumpositive_body_steps_summand + S (fs_a_dst_anti_first_sumpositive_body_steps) = S ((S (fs_i_dst_anti_first_sumpositive_body_steps)) * dst_positive_scale_anti_first_sum)) /\ exists fs_q_dst_anti_first_sumpositive_body_steps_summand. dst_positive_code_anti_first_sum = fs_q_dst_anti_first_sumpositive_body_steps_summand * S ((S (fs_i_dst_anti_first_sumpositive_body_steps)) * dst_positive_scale_anti_first_sum) + (fs_a_dst_anti_first_sumpositive_body_steps))) /\ ((((exists fs_h_dst_anti_first_sumpositive_body_steps_partial. fs_h_dst_anti_first_sumpositive_body_steps_partial + S (fs_r_dst_anti_first_sumpositive_body_steps) = S ((S (fs_i_dst_anti_first_sumpositive_body_steps)) * fs_v_dst_anti_first_sumpositive)) /\ exists fs_q_dst_anti_first_sumpositive_body_steps_partial. fs_u_dst_anti_first_sumpositive = fs_q_dst_anti_first_sumpositive_body_steps_partial * S ((S (fs_i_dst_anti_first_sumpositive_body_steps)) * fs_v_dst_anti_first_sumpositive) + (fs_r_dst_anti_first_sumpositive_body_steps))) /\ ((((exists fs_h_dst_anti_first_sumpositive_body_steps_successor. fs_h_dst_anti_first_sumpositive_body_steps_successor + S (fs_s_dst_anti_first_sumpositive_body_steps) = S ((S (S fs_i_dst_anti_first_sumpositive_body_steps)) * fs_v_dst_anti_first_sumpositive)) /\ exists fs_q_dst_anti_first_sumpositive_body_steps_successor. fs_u_dst_anti_first_sumpositive = fs_q_dst_anti_first_sumpositive_body_steps_successor * S ((S (S fs_i_dst_anti_first_sumpositive_body_steps)) * fs_v_dst_anti_first_sumpositive) + (fs_s_dst_anti_first_sumpositive_body_steps))) /\ fs_s_dst_anti_first_sumpositive_body_steps = fs_r_dst_anti_first_sumpositive_body_steps + fs_a_dst_anti_first_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_anti_first_sumnegative fs_v_dst_anti_first_sumnegative. ((((exists fs_h_dst_anti_first_sumnegative_body_start. fs_h_dst_anti_first_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_anti_first_sumnegative)) /\ exists fs_q_dst_anti_first_sumnegative_body_start. fs_u_dst_anti_first_sumnegative = fs_q_dst_anti_first_sumnegative_body_start * S ((S (0)) * fs_v_dst_anti_first_sumnegative) + (0))) /\ ((((exists fs_h_dst_anti_first_sumnegative_body_terminal. fs_h_dst_anti_first_sumnegative_body_terminal + S (dst_negative_sum_anti_first_sum) = S ((S (l)) * fs_v_dst_anti_first_sumnegative)) /\ exists fs_q_dst_anti_first_sumnegative_body_terminal. fs_u_dst_anti_first_sumnegative = fs_q_dst_anti_first_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_anti_first_sumnegative) + (dst_negative_sum_anti_first_sum))) /\ forall fs_i_dst_anti_first_sumnegative_body_steps. (exists fs_lt_dst_anti_first_sumnegative_body_steps_bound. fs_lt_dst_anti_first_sumnegative_body_steps_bound + S fs_i_dst_anti_first_sumnegative_body_steps = l) -> exists fs_a_dst_anti_first_sumnegative_body_steps fs_r_dst_anti_first_sumnegative_body_steps fs_s_dst_anti_first_sumnegative_body_steps. ((((exists fs_h_dst_anti_first_sumnegative_body_steps_summand. fs_h_dst_anti_first_sumnegative_body_steps_summand + S (fs_a_dst_anti_first_sumnegative_body_steps) = S ((S (fs_i_dst_anti_first_sumnegative_body_steps)) * dst_negative_scale_anti_first_sum)) /\ exists fs_q_dst_anti_first_sumnegative_body_steps_summand. dst_negative_code_anti_first_sum = fs_q_dst_anti_first_sumnegative_body_steps_summand * S ((S (fs_i_dst_anti_first_sumnegative_body_steps)) * dst_negative_scale_anti_first_sum) + (fs_a_dst_anti_first_sumnegative_body_steps))) /\ ((((exists fs_h_dst_anti_first_sumnegative_body_steps_partial. fs_h_dst_anti_first_sumnegative_body_steps_partial + S (fs_r_dst_anti_first_sumnegative_body_steps) = S ((S (fs_i_dst_anti_first_sumnegative_body_steps)) * fs_v_dst_anti_first_sumnegative)) /\ exists fs_q_dst_anti_first_sumnegative_body_steps_partial. fs_u_dst_anti_first_sumnegative = fs_q_dst_anti_first_sumnegative_body_steps_partial * S ((S (fs_i_dst_anti_first_sumnegative_body_steps)) * fs_v_dst_anti_first_sumnegative) + (fs_r_dst_anti_first_sumnegative_body_steps))) /\ ((((exists fs_h_dst_anti_first_sumnegative_body_steps_successor. fs_h_dst_anti_first_sumnegative_body_steps_successor + S (fs_s_dst_anti_first_sumnegative_body_steps) = S ((S (S fs_i_dst_anti_first_sumnegative_body_steps)) * fs_v_dst_anti_first_sumnegative)) /\ exists fs_q_dst_anti_first_sumnegative_body_steps_successor. fs_u_dst_anti_first_sumnegative = fs_q_dst_anti_first_sumnegative_body_steps_successor * S ((S (S fs_i_dst_anti_first_sumnegative_body_steps)) * fs_v_dst_anti_first_sumnegative) + (fs_s_dst_anti_first_sumnegative_body_steps))) /\ fs_s_dst_anti_first_sumnegative_body_steps = fs_r_dst_anti_first_sumnegative_body_steps + fs_a_dst_anti_first_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_anti_first_sumresult ge_balance_negative_anti_first_sumresult. (((((a) = 2 * (ge_balance_positive_anti_first_sumresult) /\ (ge_balance_negative_anti_first_sumresult) = 0) \/ exists ge_signed_half_anti_first_sumresultdecode. (((a) = 2 * ge_signed_half_anti_first_sumresultdecode + 1 /\ (ge_balance_positive_anti_first_sumresult) = 0) /\ (ge_balance_negative_anti_first_sumresult) = S ge_signed_half_anti_first_sumresultdecode))) /\ ((dst_positive_sum_anti_first_sum) + ge_balance_negative_anti_first_sumresult = (dst_negative_sum_anti_first_sum) + ge_balance_positive_anti_first_sumresult))))))))) -> (exists dst_positive_code_anti_second_sum dst_positive_scale_anti_second_sum dst_negative_code_anti_second_sum dst_negative_scale_anti_second_sum dst_positive_sum_anti_second_sum dst_negative_sum_anti_second_sum. (((G) = (((((dst_positive_code_anti_second_sum) + (dst_positive_scale_anti_second_sum)) * S ((dst_positive_code_anti_second_sum) + (dst_positive_scale_anti_second_sum)) + ((dst_positive_scale_anti_second_sum) + (dst_positive_scale_anti_second_sum))) + (((dst_negative_code_anti_second_sum) + (dst_negative_scale_anti_second_sum)) * S ((dst_negative_code_anti_second_sum) + (dst_negative_scale_anti_second_sum)) + ((dst_negative_scale_anti_second_sum) + (dst_negative_scale_anti_second_sum)))) * S ((((dst_positive_code_anti_second_sum) + (dst_positive_scale_anti_second_sum)) * S ((dst_positive_code_anti_second_sum) + (dst_positive_scale_anti_second_sum)) + ((dst_positive_scale_anti_second_sum) + (dst_positive_scale_anti_second_sum))) + (((dst_negative_code_anti_second_sum) + (dst_negative_scale_anti_second_sum)) * S ((dst_negative_code_anti_second_sum) + (dst_negative_scale_anti_second_sum)) + ((dst_negative_scale_anti_second_sum) + (dst_negative_scale_anti_second_sum)))) + ((((dst_negative_code_anti_second_sum) + (dst_negative_scale_anti_second_sum)) * S ((dst_negative_code_anti_second_sum) + (dst_negative_scale_anti_second_sum)) + ((dst_negative_scale_anti_second_sum) + (dst_negative_scale_anti_second_sum))) + (((dst_negative_code_anti_second_sum) + (dst_negative_scale_anti_second_sum)) * S ((dst_negative_code_anti_second_sum) + (dst_negative_scale_anti_second_sum)) + ((dst_negative_scale_anti_second_sum) + (dst_negative_scale_anti_second_sum)))))) /\ (((exists fs_u_dst_anti_second_sumpositive fs_v_dst_anti_second_sumpositive. ((((exists fs_h_dst_anti_second_sumpositive_body_start. fs_h_dst_anti_second_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_anti_second_sumpositive)) /\ exists fs_q_dst_anti_second_sumpositive_body_start. fs_u_dst_anti_second_sumpositive = fs_q_dst_anti_second_sumpositive_body_start * S ((S (0)) * fs_v_dst_anti_second_sumpositive) + (0))) /\ ((((exists fs_h_dst_anti_second_sumpositive_body_terminal. fs_h_dst_anti_second_sumpositive_body_terminal + S (dst_positive_sum_anti_second_sum) = S ((S (l)) * fs_v_dst_anti_second_sumpositive)) /\ exists fs_q_dst_anti_second_sumpositive_body_terminal. fs_u_dst_anti_second_sumpositive = fs_q_dst_anti_second_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_anti_second_sumpositive) + (dst_positive_sum_anti_second_sum))) /\ forall fs_i_dst_anti_second_sumpositive_body_steps. (exists fs_lt_dst_anti_second_sumpositive_body_steps_bound. fs_lt_dst_anti_second_sumpositive_body_steps_bound + S fs_i_dst_anti_second_sumpositive_body_steps = l) -> exists fs_a_dst_anti_second_sumpositive_body_steps fs_r_dst_anti_second_sumpositive_body_steps fs_s_dst_anti_second_sumpositive_body_steps. ((((exists fs_h_dst_anti_second_sumpositive_body_steps_summand. fs_h_dst_anti_second_sumpositive_body_steps_summand + S (fs_a_dst_anti_second_sumpositive_body_steps) = S ((S (fs_i_dst_anti_second_sumpositive_body_steps)) * dst_positive_scale_anti_second_sum)) /\ exists fs_q_dst_anti_second_sumpositive_body_steps_summand. dst_positive_code_anti_second_sum = fs_q_dst_anti_second_sumpositive_body_steps_summand * S ((S (fs_i_dst_anti_second_sumpositive_body_steps)) * dst_positive_scale_anti_second_sum) + (fs_a_dst_anti_second_sumpositive_body_steps))) /\ ((((exists fs_h_dst_anti_second_sumpositive_body_steps_partial. fs_h_dst_anti_second_sumpositive_body_steps_partial + S (fs_r_dst_anti_second_sumpositive_body_steps) = S ((S (fs_i_dst_anti_second_sumpositive_body_steps)) * fs_v_dst_anti_second_sumpositive)) /\ exists fs_q_dst_anti_second_sumpositive_body_steps_partial. fs_u_dst_anti_second_sumpositive = fs_q_dst_anti_second_sumpositive_body_steps_partial * S ((S (fs_i_dst_anti_second_sumpositive_body_steps)) * fs_v_dst_anti_second_sumpositive) + (fs_r_dst_anti_second_sumpositive_body_steps))) /\ ((((exists fs_h_dst_anti_second_sumpositive_body_steps_successor. fs_h_dst_anti_second_sumpositive_body_steps_successor + S (fs_s_dst_anti_second_sumpositive_body_steps) = S ((S (S fs_i_dst_anti_second_sumpositive_body_steps)) * fs_v_dst_anti_second_sumpositive)) /\ exists fs_q_dst_anti_second_sumpositive_body_steps_successor. fs_u_dst_anti_second_sumpositive = fs_q_dst_anti_second_sumpositive_body_steps_successor * S ((S (S fs_i_dst_anti_second_sumpositive_body_steps)) * fs_v_dst_anti_second_sumpositive) + (fs_s_dst_anti_second_sumpositive_body_steps))) /\ fs_s_dst_anti_second_sumpositive_body_steps = fs_r_dst_anti_second_sumpositive_body_steps + fs_a_dst_anti_second_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_anti_second_sumnegative fs_v_dst_anti_second_sumnegative. ((((exists fs_h_dst_anti_second_sumnegative_body_start. fs_h_dst_anti_second_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_anti_second_sumnegative)) /\ exists fs_q_dst_anti_second_sumnegative_body_start. fs_u_dst_anti_second_sumnegative = fs_q_dst_anti_second_sumnegative_body_start * S ((S (0)) * fs_v_dst_anti_second_sumnegative) + (0))) /\ ((((exists fs_h_dst_anti_second_sumnegative_body_terminal. fs_h_dst_anti_second_sumnegative_body_terminal + S (dst_negative_sum_anti_second_sum) = S ((S (l)) * fs_v_dst_anti_second_sumnegative)) /\ exists fs_q_dst_anti_second_sumnegative_body_terminal. fs_u_dst_anti_second_sumnegative = fs_q_dst_anti_second_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_anti_second_sumnegative) + (dst_negative_sum_anti_second_sum))) /\ forall fs_i_dst_anti_second_sumnegative_body_steps. (exists fs_lt_dst_anti_second_sumnegative_body_steps_bound. fs_lt_dst_anti_second_sumnegative_body_steps_bound + S fs_i_dst_anti_second_sumnegative_body_steps = l) -> exists fs_a_dst_anti_second_sumnegative_body_steps fs_r_dst_anti_second_sumnegative_body_steps fs_s_dst_anti_second_sumnegative_body_steps. ((((exists fs_h_dst_anti_second_sumnegative_body_steps_summand. fs_h_dst_anti_second_sumnegative_body_steps_summand + S (fs_a_dst_anti_second_sumnegative_body_steps) = S ((S (fs_i_dst_anti_second_sumnegative_body_steps)) * dst_negative_scale_anti_second_sum)) /\ exists fs_q_dst_anti_second_sumnegative_body_steps_summand. dst_negative_code_anti_second_sum = fs_q_dst_anti_second_sumnegative_body_steps_summand * S ((S (fs_i_dst_anti_second_sumnegative_body_steps)) * dst_negative_scale_anti_second_sum) + (fs_a_dst_anti_second_sumnegative_body_steps))) /\ ((((exists fs_h_dst_anti_second_sumnegative_body_steps_partial. fs_h_dst_anti_second_sumnegative_body_steps_partial + S (fs_r_dst_anti_second_sumnegative_body_steps) = S ((S (fs_i_dst_anti_second_sumnegative_body_steps)) * fs_v_dst_anti_second_sumnegative)) /\ exists fs_q_dst_anti_second_sumnegative_body_steps_partial. fs_u_dst_anti_second_sumnegative = fs_q_dst_anti_second_sumnegative_body_steps_partial * S ((S (fs_i_dst_anti_second_sumnegative_body_steps)) * fs_v_dst_anti_second_sumnegative) + (fs_r_dst_anti_second_sumnegative_body_steps))) /\ ((((exists fs_h_dst_anti_second_sumnegative_body_steps_successor. fs_h_dst_anti_second_sumnegative_body_steps_successor + S (fs_s_dst_anti_second_sumnegative_body_steps) = S ((S (S fs_i_dst_anti_second_sumnegative_body_steps)) * fs_v_dst_anti_second_sumnegative)) /\ exists fs_q_dst_anti_second_sumnegative_body_steps_successor. fs_u_dst_anti_second_sumnegative = fs_q_dst_anti_second_sumnegative_body_steps_successor * S ((S (S fs_i_dst_anti_second_sumnegative_body_steps)) * fs_v_dst_anti_second_sumnegative) + (fs_s_dst_anti_second_sumnegative_body_steps))) /\ fs_s_dst_anti_second_sumnegative_body_steps = fs_r_dst_anti_second_sumnegative_body_steps + fs_a_dst_anti_second_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_anti_second_sumresult ge_balance_negative_anti_second_sumresult. (((((b) = 2 * (ge_balance_positive_anti_second_sumresult) /\ (ge_balance_negative_anti_second_sumresult) = 0) \/ exists ge_signed_half_anti_second_sumresultdecode. (((b) = 2 * ge_signed_half_anti_second_sumresultdecode + 1 /\ (ge_balance_positive_anti_second_sumresult) = 0) /\ (ge_balance_negative_anti_second_sumresult) = S ge_signed_half_anti_second_sumresultdecode))) /\ ((dst_positive_sum_anti_second_sum) + ge_balance_negative_anti_second_sumresult = (dst_negative_sum_anti_second_sum) + ge_balance_positive_anti_second_sumresult))))))))) -> a=0