divisor_signed_sum_component_reindex

Exact expanded first-order arithmetic statement

forall F G pb pc nb nc qb qc mb mc r s l u v. ((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)))))) -> ((G) = (((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) * S ((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) + ((((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))))) -> (forall pfp_i_sum_map_bounded. (exists pfp_gap_sum_map_boundedindex. pfp_gap_sum_map_boundedindex + S (pfp_i_sum_map_bounded) = (l)) -> exists pfp_a_sum_map_bounded. (((exists ff_h_pfp_sum_map_boundedentry. ff_h_pfp_sum_map_boundedentry + S (pfp_a_sum_map_bounded) = S ((S (pfp_i_sum_map_bounded)) * s)) /\ exists ff_q_pfp_sum_map_boundedentry. r = ff_q_pfp_sum_map_boundedentry * S ((S (pfp_i_sum_map_bounded)) * s) + (pfp_a_sum_map_bounded))) /\ (exists pfp_gap_sum_map_boundedvalue. pfp_gap_sum_map_boundedvalue + S (pfp_a_sum_map_bounded) = (l))) -> (forall pfp_i_sum_map_injective pfp_j_sum_map_injective pfp_a_sum_map_injective. (exists pfp_gap_sum_map_injectivefirst. pfp_gap_sum_map_injectivefirst + S (pfp_i_sum_map_injective) = (l)) -> (exists pfp_gap_sum_map_injectivesecond. pfp_gap_sum_map_injectivesecond + S (pfp_j_sum_map_injective) = (l)) -> (((exists ff_h_pfp_sum_map_injectiveleft. ff_h_pfp_sum_map_injectiveleft + S (pfp_a_sum_map_injective) = S ((S (pfp_i_sum_map_injective)) * s)) /\ exists ff_q_pfp_sum_map_injectiveleft. r = ff_q_pfp_sum_map_injectiveleft * S ((S (pfp_i_sum_map_injective)) * s) + (pfp_a_sum_map_injective))) -> (((exists ff_h_pfp_sum_map_injectiveright. ff_h_pfp_sum_map_injectiveright + S (pfp_a_sum_map_injective) = S ((S (pfp_j_sum_map_injective)) * s)) /\ exists ff_q_pfp_sum_map_injectiveright. r = ff_q_pfp_sum_map_injectiveright * S ((S (pfp_j_sum_map_injective)) * s) + (pfp_a_sum_map_injective))) -> pfp_i_sum_map_injective = pfp_j_sum_map_injective) -> (((forall fms_i_sum_component_compositionpositive fms_j_sum_component_compositionpositive fms_v_sum_component_compositionpositive. (exists fms_gap_sum_component_compositionpositive. fms_gap_sum_component_compositionpositive + S (fms_i_sum_component_compositionpositive) = (l)) -> (((exists fs_h_fms_sum_component_compositionpositive_index. fs_h_fms_sum_component_compositionpositive_index + S (fms_j_sum_component_compositionpositive) = S ((S (fms_i_sum_component_compositionpositive)) * s)) /\ exists fs_q_fms_sum_component_compositionpositive_index. r = fs_q_fms_sum_component_compositionpositive_index * S ((S (fms_i_sum_component_compositionpositive)) * s) + (fms_j_sum_component_compositionpositive))) -> (((exists fs_h_fms_sum_component_compositionpositive_source. fs_h_fms_sum_component_compositionpositive_source + S (fms_v_sum_component_compositionpositive) = S ((S (fms_j_sum_component_compositionpositive)) * pc)) /\ exists fs_q_fms_sum_component_compositionpositive_source. pb = fs_q_fms_sum_component_compositionpositive_source * S ((S (fms_j_sum_component_compositionpositive)) * pc) + (fms_v_sum_component_compositionpositive))) -> (((exists fs_h_fms_sum_component_compositionpositive_target. fs_h_fms_sum_component_compositionpositive_target + S (fms_v_sum_component_compositionpositive) = S ((S (fms_i_sum_component_compositionpositive)) * qc)) /\ exists fs_q_fms_sum_component_compositionpositive_target. qb = fs_q_fms_sum_component_compositionpositive_target * S ((S (fms_i_sum_component_compositionpositive)) * qc) + (fms_v_sum_component_compositionpositive)))) /\ (forall fms_i_sum_component_compositionnegative fms_j_sum_component_compositionnegative fms_v_sum_component_compositionnegative. (exists fms_gap_sum_component_compositionnegative. fms_gap_sum_component_compositionnegative + S (fms_i_sum_component_compositionnegative) = (l)) -> (((exists fs_h_fms_sum_component_compositionnegative_index. fs_h_fms_sum_component_compositionnegative_index + S (fms_j_sum_component_compositionnegative) = S ((S (fms_i_sum_component_compositionnegative)) * s)) /\ exists fs_q_fms_sum_component_compositionnegative_index. r = fs_q_fms_sum_component_compositionnegative_index * S ((S (fms_i_sum_component_compositionnegative)) * s) + (fms_j_sum_component_compositionnegative))) -> (((exists fs_h_fms_sum_component_compositionnegative_source. fs_h_fms_sum_component_compositionnegative_source + S (fms_v_sum_component_compositionnegative) = S ((S (fms_j_sum_component_compositionnegative)) * nc)) /\ exists fs_q_fms_sum_component_compositionnegative_source. nb = fs_q_fms_sum_component_compositionnegative_source * S ((S (fms_j_sum_component_compositionnegative)) * nc) + (fms_v_sum_component_compositionnegative))) -> (((exists fs_h_fms_sum_component_compositionnegative_target. fs_h_fms_sum_component_compositionnegative_target + S (fms_v_sum_component_compositionnegative) = S ((S (fms_i_sum_component_compositionnegative)) * mc)) /\ exists fs_q_fms_sum_component_compositionnegative_target. mb = fs_q_fms_sum_component_compositionnegative_target * S ((S (fms_i_sum_component_compositionnegative)) * mc) + (fms_v_sum_component_compositionnegative)))))) -> (exists dst_positive_code_sum_source dst_positive_scale_sum_source dst_negative_code_sum_source dst_negative_scale_sum_source dst_positive_sum_sum_source dst_negative_sum_sum_source. (((F) = (((((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) * S ((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) + ((dst_positive_scale_sum_source) + (dst_positive_scale_sum_source))) + (((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source)))) * S ((((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) * S ((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) + ((dst_positive_scale_sum_source) + (dst_positive_scale_sum_source))) + (((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source)))) + ((((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source))) + (((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source)))))) /\ (((exists fs_u_dst_sum_sourcepositive fs_v_dst_sum_sourcepositive. ((((exists fs_h_dst_sum_sourcepositive_body_start. fs_h_dst_sum_sourcepositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_start. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_start * S ((S (0)) * fs_v_dst_sum_sourcepositive) + (0))) /\ ((((exists fs_h_dst_sum_sourcepositive_body_terminal. fs_h_dst_sum_sourcepositive_body_terminal + S (dst_positive_sum_sum_source) = S ((S (l)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_terminal. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_terminal * S ((S (l)) * fs_v_dst_sum_sourcepositive) + (dst_positive_sum_sum_source))) /\ forall fs_i_dst_sum_sourcepositive_body_steps. (exists fs_lt_dst_sum_sourcepositive_body_steps_bound. fs_lt_dst_sum_sourcepositive_body_steps_bound + S fs_i_dst_sum_sourcepositive_body_steps = l) -> exists fs_a_dst_sum_sourcepositive_body_steps fs_r_dst_sum_sourcepositive_body_steps fs_s_dst_sum_sourcepositive_body_steps. ((((exists fs_h_dst_sum_sourcepositive_body_steps_summand. fs_h_dst_sum_sourcepositive_body_steps_summand + S (fs_a_dst_sum_sourcepositive_body_steps) = S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * dst_positive_scale_sum_source)) /\ exists fs_q_dst_sum_sourcepositive_body_steps_summand. dst_positive_code_sum_source = fs_q_dst_sum_sourcepositive_body_steps_summand * S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * dst_positive_scale_sum_source) + (fs_a_dst_sum_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_sum_sourcepositive_body_steps_partial. fs_h_dst_sum_sourcepositive_body_steps_partial + S (fs_r_dst_sum_sourcepositive_body_steps) = S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_steps_partial. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_steps_partial * S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive) + (fs_r_dst_sum_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_sum_sourcepositive_body_steps_successor. fs_h_dst_sum_sourcepositive_body_steps_successor + S (fs_s_dst_sum_sourcepositive_body_steps) = S ((S (S fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_steps_successor. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_steps_successor * S ((S (S fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive) + (fs_s_dst_sum_sourcepositive_body_steps))) /\ fs_s_dst_sum_sourcepositive_body_steps = fs_r_dst_sum_sourcepositive_body_steps + fs_a_dst_sum_sourcepositive_body_steps)))))) /\ (((exists fs_u_dst_sum_sourcenegative fs_v_dst_sum_sourcenegative. ((((exists fs_h_dst_sum_sourcenegative_body_start. fs_h_dst_sum_sourcenegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_start. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_start * S ((S (0)) * fs_v_dst_sum_sourcenegative) + (0))) /\ ((((exists fs_h_dst_sum_sourcenegative_body_terminal. fs_h_dst_sum_sourcenegative_body_terminal + S (dst_negative_sum_sum_source) = S ((S (l)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_terminal. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_terminal * S ((S (l)) * fs_v_dst_sum_sourcenegative) + (dst_negative_sum_sum_source))) /\ forall fs_i_dst_sum_sourcenegative_body_steps. (exists fs_lt_dst_sum_sourcenegative_body_steps_bound. fs_lt_dst_sum_sourcenegative_body_steps_bound + S fs_i_dst_sum_sourcenegative_body_steps = l) -> exists fs_a_dst_sum_sourcenegative_body_steps fs_r_dst_sum_sourcenegative_body_steps fs_s_dst_sum_sourcenegative_body_steps. ((((exists fs_h_dst_sum_sourcenegative_body_steps_summand. fs_h_dst_sum_sourcenegative_body_steps_summand + S (fs_a_dst_sum_sourcenegative_body_steps) = S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * dst_negative_scale_sum_source)) /\ exists fs_q_dst_sum_sourcenegative_body_steps_summand. dst_negative_code_sum_source = fs_q_dst_sum_sourcenegative_body_steps_summand * S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * dst_negative_scale_sum_source) + (fs_a_dst_sum_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_sum_sourcenegative_body_steps_partial. fs_h_dst_sum_sourcenegative_body_steps_partial + S (fs_r_dst_sum_sourcenegative_body_steps) = S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_steps_partial. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_steps_partial * S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative) + (fs_r_dst_sum_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_sum_sourcenegative_body_steps_successor. fs_h_dst_sum_sourcenegative_body_steps_successor + S (fs_s_dst_sum_sourcenegative_body_steps) = S ((S (S fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_steps_successor. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_steps_successor * S ((S (S fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative) + (fs_s_dst_sum_sourcenegative_body_steps))) /\ fs_s_dst_sum_sourcenegative_body_steps = fs_r_dst_sum_sourcenegative_body_steps + fs_a_dst_sum_sourcenegative_body_steps)))))) /\ (exists ge_balance_positive_sum_sourceresult ge_balance_negative_sum_sourceresult. (((((u) = 2 * (ge_balance_positive_sum_sourceresult) /\ (ge_balance_negative_sum_sourceresult) = 0) \/ exists ge_signed_half_sum_sourceresultdecode. (((u) = 2 * ge_signed_half_sum_sourceresultdecode + 1 /\ (ge_balance_positive_sum_sourceresult) = 0) /\ (ge_balance_negative_sum_sourceresult) = S ge_signed_half_sum_sourceresultdecode))) /\ ((dst_positive_sum_sum_source) + ge_balance_negative_sum_sourceresult = (dst_negative_sum_sum_source) + ge_balance_positive_sum_sourceresult))))))))) -> (exists dst_positive_code_sum_target dst_positive_scale_sum_target dst_negative_code_sum_target dst_negative_scale_sum_target dst_positive_sum_sum_target dst_negative_sum_sum_target. (((G) = (((((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) * S ((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) + ((dst_positive_scale_sum_target) + (dst_positive_scale_sum_target))) + (((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target)))) * S ((((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) * S ((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) + ((dst_positive_scale_sum_target) + (dst_positive_scale_sum_target))) + (((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target)))) + ((((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target))) + (((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target)))))) /\ (((exists fs_u_dst_sum_targetpositive fs_v_dst_sum_targetpositive. ((((exists fs_h_dst_sum_targetpositive_body_start. fs_h_dst_sum_targetpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_start. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_start * S ((S (0)) * fs_v_dst_sum_targetpositive) + (0))) /\ ((((exists fs_h_dst_sum_targetpositive_body_terminal. fs_h_dst_sum_targetpositive_body_terminal + S (dst_positive_sum_sum_target) = S ((S (l)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_terminal. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_targetpositive) + (dst_positive_sum_sum_target))) /\ forall fs_i_dst_sum_targetpositive_body_steps. (exists fs_lt_dst_sum_targetpositive_body_steps_bound. fs_lt_dst_sum_targetpositive_body_steps_bound + S fs_i_dst_sum_targetpositive_body_steps = l) -> exists fs_a_dst_sum_targetpositive_body_steps fs_r_dst_sum_targetpositive_body_steps fs_s_dst_sum_targetpositive_body_steps. ((((exists fs_h_dst_sum_targetpositive_body_steps_summand. fs_h_dst_sum_targetpositive_body_steps_summand + S (fs_a_dst_sum_targetpositive_body_steps) = S ((S (fs_i_dst_sum_targetpositive_body_steps)) * dst_positive_scale_sum_target)) /\ exists fs_q_dst_sum_targetpositive_body_steps_summand. dst_positive_code_sum_target = fs_q_dst_sum_targetpositive_body_steps_summand * S ((S (fs_i_dst_sum_targetpositive_body_steps)) * dst_positive_scale_sum_target) + (fs_a_dst_sum_targetpositive_body_steps))) /\ ((((exists fs_h_dst_sum_targetpositive_body_steps_partial. fs_h_dst_sum_targetpositive_body_steps_partial + S (fs_r_dst_sum_targetpositive_body_steps) = S ((S (fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_steps_partial. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_steps_partial * S ((S (fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive) + (fs_r_dst_sum_targetpositive_body_steps))) /\ ((((exists fs_h_dst_sum_targetpositive_body_steps_successor. fs_h_dst_sum_targetpositive_body_steps_successor + S (fs_s_dst_sum_targetpositive_body_steps) = S ((S (S fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_steps_successor. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_steps_successor * S ((S (S fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive) + (fs_s_dst_sum_targetpositive_body_steps))) /\ fs_s_dst_sum_targetpositive_body_steps = fs_r_dst_sum_targetpositive_body_steps + fs_a_dst_sum_targetpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_targetnegative fs_v_dst_sum_targetnegative. ((((exists fs_h_dst_sum_targetnegative_body_start. fs_h_dst_sum_targetnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_start. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_start * S ((S (0)) * fs_v_dst_sum_targetnegative) + (0))) /\ ((((exists fs_h_dst_sum_targetnegative_body_terminal. fs_h_dst_sum_targetnegative_body_terminal + S (dst_negative_sum_sum_target) = S ((S (l)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_terminal. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_targetnegative) + (dst_negative_sum_sum_target))) /\ forall fs_i_dst_sum_targetnegative_body_steps. (exists fs_lt_dst_sum_targetnegative_body_steps_bound. fs_lt_dst_sum_targetnegative_body_steps_bound + S fs_i_dst_sum_targetnegative_body_steps = l) -> exists fs_a_dst_sum_targetnegative_body_steps fs_r_dst_sum_targetnegative_body_steps fs_s_dst_sum_targetnegative_body_steps. ((((exists fs_h_dst_sum_targetnegative_body_steps_summand. fs_h_dst_sum_targetnegative_body_steps_summand + S (fs_a_dst_sum_targetnegative_body_steps) = S ((S (fs_i_dst_sum_targetnegative_body_steps)) * dst_negative_scale_sum_target)) /\ exists fs_q_dst_sum_targetnegative_body_steps_summand. dst_negative_code_sum_target = fs_q_dst_sum_targetnegative_body_steps_summand * S ((S (fs_i_dst_sum_targetnegative_body_steps)) * dst_negative_scale_sum_target) + (fs_a_dst_sum_targetnegative_body_steps))) /\ ((((exists fs_h_dst_sum_targetnegative_body_steps_partial. fs_h_dst_sum_targetnegative_body_steps_partial + S (fs_r_dst_sum_targetnegative_body_steps) = S ((S (fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_steps_partial. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_steps_partial * S ((S (fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative) + (fs_r_dst_sum_targetnegative_body_steps))) /\ ((((exists fs_h_dst_sum_targetnegative_body_steps_successor. fs_h_dst_sum_targetnegative_body_steps_successor + S (fs_s_dst_sum_targetnegative_body_steps) = S ((S (S fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_steps_successor. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_steps_successor * S ((S (S fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative) + (fs_s_dst_sum_targetnegative_body_steps))) /\ fs_s_dst_sum_targetnegative_body_steps = fs_r_dst_sum_targetnegative_body_steps + fs_a_dst_sum_targetnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_targetresult ge_balance_negative_sum_targetresult. (((((v) = 2 * (ge_balance_positive_sum_targetresult) /\ (ge_balance_negative_sum_targetresult) = 0) \/ exists ge_signed_half_sum_targetresultdecode. (((v) = 2 * ge_signed_half_sum_targetresultdecode + 1 /\ (ge_balance_positive_sum_targetresult) = 0) /\ (ge_balance_negative_sum_targetresult) = S ge_signed_half_sum_targetresultdecode))) /\ ((dst_positive_sum_sum_target) + ge_balance_negative_sum_targetresult = (dst_negative_sum_sum_target) + ge_balance_positive_sum_targetresult))))))))) -> u = v