gauss_eisenstein_terminal_cancel_magnitude_mod_two

Exact expanded PA statement

forall p h a b c tb tc qb qc rb rc mb mc sb sc X Q M E. ((~(p = 1) /\ forall gsp_prime_left_ges_prime gsp_prime_right_ges_prime. p = gsp_prime_left_ges_prime * gsp_prime_right_ges_prime -> gsp_prime_left_ges_prime = 1 \/ gsp_prime_right_ges_prime = 1)) -> (~(exists gsp_divisor_factor_ges_nondivisor. a = p * gsp_divisor_factor_ges_nondivisor)) -> p = 2 * h + 1 -> (exists sdp_odd_ges_scale. a = 2 * sdp_odd_ges_scale + 1) -> (forall gsp_range_index_ges_half. (exists gsp_lt_gap_ges_half_range_bound. gsp_lt_gap_ges_half_range_bound + S gsp_range_index_ges_half = h) -> (((exists gsp_beta_height_ges_half_range_entry. gsp_beta_height_ges_half_range_entry + S (1 + gsp_range_index_ges_half) = S ((S (gsp_range_index_ges_half)) * c)) /\ exists gsp_beta_quotient_ges_half_range_entry. b = gsp_beta_quotient_ges_half_range_entry * S ((S (gsp_range_index_ges_half)) * c) + (1 + gsp_range_index_ges_half)))) -> (forall esd_index_ges_scaled esd_value_ges_scaled. (exists esd_gap_ges_scaled. esd_gap_ges_scaled + S esd_index_ges_scaled = h) -> (((exists ff_h_esd_ges_scaled_decoded. ff_h_esd_ges_scaled_decoded + S (esd_value_ges_scaled) = S ((S (esd_index_ges_scaled)) * tc)) /\ exists ff_q_esd_ges_scaled_decoded. tb = ff_q_esd_ges_scaled_decoded * S ((S (esd_index_ges_scaled)) * tc) + (esd_value_ges_scaled))) -> esd_value_ges_scaled = a * (1 + esd_index_ges_scaled)) -> (forall fdp_index_ges_division. (exists gsp_lt_gap_ges_division_index_bound. gsp_lt_gap_ges_division_index_bound + S fdp_index_ges_division = h) -> exists fdp_value_ges_division fdp_quotient_ges_division fdp_remainder_ges_division. (((exists ff_h_fdp_ges_division_source. ff_h_fdp_ges_division_source + S (fdp_value_ges_division) = S ((S (fdp_index_ges_division)) * tc)) /\ exists ff_q_fdp_ges_division_source. tb = ff_q_fdp_ges_division_source * S ((S (fdp_index_ges_division)) * tc) + (fdp_value_ges_division))) /\ ((((exists ff_h_fdp_ges_division_quotient_entry. ff_h_fdp_ges_division_quotient_entry + S (fdp_quotient_ges_division) = S ((S (fdp_index_ges_division)) * qc)) /\ exists ff_q_fdp_ges_division_quotient_entry. qb = ff_q_fdp_ges_division_quotient_entry * S ((S (fdp_index_ges_division)) * qc) + (fdp_quotient_ges_division))) /\ ((((exists ff_h_fdp_ges_division_remainder_entry. ff_h_fdp_ges_division_remainder_entry + S (fdp_remainder_ges_division) = S ((S (fdp_index_ges_division)) * rc)) /\ exists ff_q_fdp_ges_division_remainder_entry. rb = ff_q_fdp_ges_division_remainder_entry * S ((S (fdp_index_ges_division)) * rc) + (fdp_remainder_ges_division))) /\ (fdp_value_ges_division = p * fdp_quotient_ges_division + fdp_remainder_ges_division /\ (exists gsp_lt_gap_ges_division_remainder_bound. gsp_lt_gap_ges_division_remainder_bound + S fdp_remainder_ges_division = p))))) -> (forall gsp_index_ges_signed. (exists gsp_lt_gap_ges_signed_index_bound. gsp_lt_gap_ges_signed_index_bound + S gsp_index_ges_signed = h) -> (exists gsp_value_ges_signed_entry gsp_magnitude_ges_signed_entry gsp_sign_ges_signed_entry. (((exists ff_h_gsp_ges_signed_entry_source. ff_h_gsp_ges_signed_entry_source + S (gsp_value_ges_signed_entry) = S ((S (gsp_index_ges_signed)) * c)) /\ exists ff_q_gsp_ges_signed_entry_source. b = ff_q_gsp_ges_signed_entry_source * S ((S (gsp_index_ges_signed)) * c) + (gsp_value_ges_signed_entry))) /\ ((((exists ff_h_gsp_ges_signed_entry_magnitude. ff_h_gsp_ges_signed_entry_magnitude + S (gsp_magnitude_ges_signed_entry) = S ((S (gsp_index_ges_signed)) * mc)) /\ exists ff_q_gsp_ges_signed_entry_magnitude. mb = ff_q_gsp_ges_signed_entry_magnitude * S ((S (gsp_index_ges_signed)) * mc) + (gsp_magnitude_ges_signed_entry))) /\ ((((exists ff_h_gsp_ges_signed_entry_sign. ff_h_gsp_ges_signed_entry_sign + S (gsp_sign_ges_signed_entry) = S ((S (gsp_index_ges_signed)) * sc)) /\ exists ff_q_gsp_ges_signed_entry_sign. sb = ff_q_gsp_ges_signed_entry_sign * S ((S (gsp_index_ges_signed)) * sc) + (gsp_sign_ges_signed_entry))) /\ ((exists gsp_lt_gap_ges_signed_entry_positive. gsp_lt_gap_ges_signed_entry_positive + S 0 = gsp_magnitude_ges_signed_entry) /\ ((exists gsp_le_gap_ges_signed_entry_bounded. gsp_le_gap_ges_signed_entry_bounded + gsp_magnitude_ges_signed_entry = h) /\ ((gsp_sign_ges_signed_entry = 0 \/ gsp_sign_ges_signed_entry = 1) /\ (((gsp_sign_ges_signed_entry = 0 /\ (exists gsp_mod_left_ges_signed_entry_lower gsp_mod_right_ges_signed_entry_lower. (a * gsp_value_ges_signed_entry) + p * gsp_mod_left_ges_signed_entry_lower = (gsp_magnitude_ges_signed_entry) + p * gsp_mod_right_ges_signed_entry_lower)) \/ (gsp_sign_ges_signed_entry = 1 /\ (exists gsp_mod_left_ges_signed_entry_reflected gsp_mod_right_ges_signed_entry_reflected. (a * gsp_value_ges_signed_entry) + p * gsp_mod_left_ges_signed_entry_reflected = ((2 * h) * gsp_magnitude_ges_signed_entry) + p * gsp_mod_right_ges_signed_entry_reflected))))))))))) -> (exists ff_u_ges_half_sum ff_v_ges_half_sum. ((((exists ff_h_ges_half_sum_start. ff_h_ges_half_sum_start + S (0) = S ((S (0)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_start. ff_u_ges_half_sum = ff_q_ges_half_sum_start * S ((S (0)) * ff_v_ges_half_sum) + (0))) /\ ((((exists ff_h_ges_half_sum_terminal. ff_h_ges_half_sum_terminal + S (X) = S ((S (h)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_terminal. ff_u_ges_half_sum = ff_q_ges_half_sum_terminal * S ((S (h)) * ff_v_ges_half_sum) + (X))) /\ forall ff_i_ges_half_sum. (exists ff_lt_ges_half_sum_bound. ff_lt_ges_half_sum_bound + S ff_i_ges_half_sum = h) -> exists ff_a_ges_half_sum ff_r_ges_half_sum ff_s_ges_half_sum. ((((exists ff_h_ges_half_sum_summand. ff_h_ges_half_sum_summand + S (ff_a_ges_half_sum) = S ((S (ff_i_ges_half_sum)) * c)) /\ exists ff_q_ges_half_sum_summand. b = ff_q_ges_half_sum_summand * S ((S (ff_i_ges_half_sum)) * c) + (ff_a_ges_half_sum))) /\ ((((exists ff_h_ges_half_sum_partial. ff_h_ges_half_sum_partial + S (ff_r_ges_half_sum) = S ((S (ff_i_ges_half_sum)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_partial. ff_u_ges_half_sum = ff_q_ges_half_sum_partial * S ((S (ff_i_ges_half_sum)) * ff_v_ges_half_sum) + (ff_r_ges_half_sum))) /\ ((((exists ff_h_ges_half_sum_successor. ff_h_ges_half_sum_successor + S (ff_s_ges_half_sum) = S ((S (S ff_i_ges_half_sum)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_successor. ff_u_ges_half_sum = ff_q_ges_half_sum_successor * S ((S (S ff_i_ges_half_sum)) * ff_v_ges_half_sum) + (ff_s_ges_half_sum))) /\ ff_s_ges_half_sum = ff_r_ges_half_sum + ff_a_ges_half_sum)))))) -> (exists ff_u_ges_quotient_sum ff_v_ges_quotient_sum. ((((exists ff_h_ges_quotient_sum_start. ff_h_ges_quotient_sum_start + S (0) = S ((S (0)) * ff_v_ges_quotient_sum)) /\ exists ff_q_ges_quotient_sum_start. ff_u_ges_quotient_sum = ff_q_ges_quotient_sum_start * S ((S (0)) * ff_v_ges_quotient_sum) + (0))) /\ ((((exists ff_h_ges_quotient_sum_terminal. ff_h_ges_quotient_sum_terminal + S (Q) = S ((S (h)) * ff_v_ges_quotient_sum)) /\ exists ff_q_ges_quotient_sum_terminal. ff_u_ges_quotient_sum = ff_q_ges_quotient_sum_terminal * S ((S (h)) * ff_v_ges_quotient_sum) + (Q))) /\ forall ff_i_ges_quotient_sum. (exists ff_lt_ges_quotient_sum_bound. ff_lt_ges_quotient_sum_bound + S ff_i_ges_quotient_sum = h) -> exists ff_a_ges_quotient_sum ff_r_ges_quotient_sum ff_s_ges_quotient_sum. ((((exists ff_h_ges_quotient_sum_summand. ff_h_ges_quotient_sum_summand + S (ff_a_ges_quotient_sum) = S ((S (ff_i_ges_quotient_sum)) * qc)) /\ exists ff_q_ges_quotient_sum_summand. qb = ff_q_ges_quotient_sum_summand * S ((S (ff_i_ges_quotient_sum)) * qc) + (ff_a_ges_quotient_sum))) /\ ((((exists ff_h_ges_quotient_sum_partial. ff_h_ges_quotient_sum_partial + S (ff_r_ges_quotient_sum) = S ((S (ff_i_ges_quotient_sum)) * ff_v_ges_quotient_sum)) /\ exists ff_q_ges_quotient_sum_partial. ff_u_ges_quotient_sum = ff_q_ges_quotient_sum_partial * S ((S (ff_i_ges_quotient_sum)) * ff_v_ges_quotient_sum) + (ff_r_ges_quotient_sum))) /\ ((((exists ff_h_ges_quotient_sum_successor. ff_h_ges_quotient_sum_successor + S (ff_s_ges_quotient_sum) = S ((S (S ff_i_ges_quotient_sum)) * ff_v_ges_quotient_sum)) /\ exists ff_q_ges_quotient_sum_successor. ff_u_ges_quotient_sum = ff_q_ges_quotient_sum_successor * S ((S (S ff_i_ges_quotient_sum)) * ff_v_ges_quotient_sum) + (ff_s_ges_quotient_sum))) /\ ff_s_ges_quotient_sum = ff_r_ges_quotient_sum + ff_a_ges_quotient_sum)))))) -> (exists ff_u_ges_magnitude_sum ff_v_ges_magnitude_sum. ((((exists ff_h_ges_magnitude_sum_start. ff_h_ges_magnitude_sum_start + S (0) = S ((S (0)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_start. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_start * S ((S (0)) * ff_v_ges_magnitude_sum) + (0))) /\ ((((exists ff_h_ges_magnitude_sum_terminal. ff_h_ges_magnitude_sum_terminal + S (M) = S ((S (h)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_terminal. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_terminal * S ((S (h)) * ff_v_ges_magnitude_sum) + (M))) /\ forall ff_i_ges_magnitude_sum. (exists ff_lt_ges_magnitude_sum_bound. ff_lt_ges_magnitude_sum_bound + S ff_i_ges_magnitude_sum = h) -> exists ff_a_ges_magnitude_sum ff_r_ges_magnitude_sum ff_s_ges_magnitude_sum. ((((exists ff_h_ges_magnitude_sum_summand. ff_h_ges_magnitude_sum_summand + S (ff_a_ges_magnitude_sum) = S ((S (ff_i_ges_magnitude_sum)) * mc)) /\ exists ff_q_ges_magnitude_sum_summand. mb = ff_q_ges_magnitude_sum_summand * S ((S (ff_i_ges_magnitude_sum)) * mc) + (ff_a_ges_magnitude_sum))) /\ ((((exists ff_h_ges_magnitude_sum_partial. ff_h_ges_magnitude_sum_partial + S (ff_r_ges_magnitude_sum) = S ((S (ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_partial. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_partial * S ((S (ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum) + (ff_r_ges_magnitude_sum))) /\ ((((exists ff_h_ges_magnitude_sum_successor. ff_h_ges_magnitude_sum_successor + S (ff_s_ges_magnitude_sum) = S ((S (S ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_successor. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_successor * S ((S (S ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum) + (ff_s_ges_magnitude_sum))) /\ ff_s_ges_magnitude_sum = ff_r_ges_magnitude_sum + ff_a_ges_magnitude_sum)))))) -> (exists ff_u_ges_sign_sum ff_v_ges_sign_sum. ((((exists ff_h_ges_sign_sum_start. ff_h_ges_sign_sum_start + S (0) = S ((S (0)) * ff_v_ges_sign_sum)) /\ exists ff_q_ges_sign_sum_start. ff_u_ges_sign_sum = ff_q_ges_sign_sum_start * S ((S (0)) * ff_v_ges_sign_sum) + (0))) /\ ((((exists ff_h_ges_sign_sum_terminal. ff_h_ges_sign_sum_terminal + S (E) = S ((S (h)) * ff_v_ges_sign_sum)) /\ exists ff_q_ges_sign_sum_terminal. ff_u_ges_sign_sum = ff_q_ges_sign_sum_terminal * S ((S (h)) * ff_v_ges_sign_sum) + (E))) /\ forall ff_i_ges_sign_sum. (exists ff_lt_ges_sign_sum_bound. ff_lt_ges_sign_sum_bound + S ff_i_ges_sign_sum = h) -> exists ff_a_ges_sign_sum ff_r_ges_sign_sum ff_s_ges_sign_sum. ((((exists ff_h_ges_sign_sum_summand. ff_h_ges_sign_sum_summand + S (ff_a_ges_sign_sum) = S ((S (ff_i_ges_sign_sum)) * sc)) /\ exists ff_q_ges_sign_sum_summand. sb = ff_q_ges_sign_sum_summand * S ((S (ff_i_ges_sign_sum)) * sc) + (ff_a_ges_sign_sum))) /\ ((((exists ff_h_ges_sign_sum_partial. ff_h_ges_sign_sum_partial + S (ff_r_ges_sign_sum) = S ((S (ff_i_ges_sign_sum)) * ff_v_ges_sign_sum)) /\ exists ff_q_ges_sign_sum_partial. ff_u_ges_sign_sum = ff_q_ges_sign_sum_partial * S ((S (ff_i_ges_sign_sum)) * ff_v_ges_sign_sum) + (ff_r_ges_sign_sum))) /\ ((((exists ff_h_ges_sign_sum_successor. ff_h_ges_sign_sum_successor + S (ff_s_ges_sign_sum) = S ((S (S ff_i_ges_sign_sum)) * ff_v_ges_sign_sum)) /\ exists ff_q_ges_sign_sum_successor. ff_u_ges_sign_sum = ff_q_ges_sign_sum_successor * S ((S (S ff_i_ges_sign_sum)) * ff_v_ges_sign_sum) + (ff_s_ges_sign_sum))) /\ ff_s_ges_sign_sum = ff_r_ges_sign_sum + ff_a_ges_sign_sum)))))) -> (exists fspm_u_ges_canceled fspm_v_ges_canceled. (0) + 2 * fspm_u_ges_canceled = (Q + E) + 2 * fspm_v_ges_canceled)