doubling_gauss_reflection_count_shape

Exact expanded first-order arithmetic statement

forall p h a b c mb mc sb sc e. p = 2 * h + 1 -> a = 2 -> (forall gsp_range_index_qst_goal_half. (exists gsp_lt_gap_qst_goal_half_range_bound. gsp_lt_gap_qst_goal_half_range_bound + S gsp_range_index_qst_goal_half = h) -> (((exists gsp_beta_height_qst_goal_half_range_entry. gsp_beta_height_qst_goal_half_range_entry + S (1 + gsp_range_index_qst_goal_half) = S ((S (gsp_range_index_qst_goal_half)) * c)) /\ exists gsp_beta_quotient_qst_goal_half_range_entry. b = gsp_beta_quotient_qst_goal_half_range_entry * S ((S (gsp_range_index_qst_goal_half)) * c) + (1 + gsp_range_index_qst_goal_half)))) -> (forall gsp_index_qst_goal_signed. (exists gsp_lt_gap_qst_goal_signed_index_bound. gsp_lt_gap_qst_goal_signed_index_bound + S gsp_index_qst_goal_signed = h) -> (exists gsp_value_qst_goal_signed_entry gsp_magnitude_qst_goal_signed_entry gsp_sign_qst_goal_signed_entry. (((exists ff_h_gsp_qst_goal_signed_entry_source. ff_h_gsp_qst_goal_signed_entry_source + S (gsp_value_qst_goal_signed_entry) = S ((S (gsp_index_qst_goal_signed)) * c)) /\ exists ff_q_gsp_qst_goal_signed_entry_source. b = ff_q_gsp_qst_goal_signed_entry_source * S ((S (gsp_index_qst_goal_signed)) * c) + (gsp_value_qst_goal_signed_entry))) /\ ((((exists ff_h_gsp_qst_goal_signed_entry_magnitude. ff_h_gsp_qst_goal_signed_entry_magnitude + S (gsp_magnitude_qst_goal_signed_entry) = S ((S (gsp_index_qst_goal_signed)) * mc)) /\ exists ff_q_gsp_qst_goal_signed_entry_magnitude. mb = ff_q_gsp_qst_goal_signed_entry_magnitude * S ((S (gsp_index_qst_goal_signed)) * mc) + (gsp_magnitude_qst_goal_signed_entry))) /\ ((((exists ff_h_gsp_qst_goal_signed_entry_sign. ff_h_gsp_qst_goal_signed_entry_sign + S (gsp_sign_qst_goal_signed_entry) = S ((S (gsp_index_qst_goal_signed)) * sc)) /\ exists ff_q_gsp_qst_goal_signed_entry_sign. sb = ff_q_gsp_qst_goal_signed_entry_sign * S ((S (gsp_index_qst_goal_signed)) * sc) + (gsp_sign_qst_goal_signed_entry))) /\ ((exists gsp_lt_gap_qst_goal_signed_entry_positive. gsp_lt_gap_qst_goal_signed_entry_positive + S 0 = gsp_magnitude_qst_goal_signed_entry) /\ ((exists gsp_le_gap_qst_goal_signed_entry_bounded. gsp_le_gap_qst_goal_signed_entry_bounded + gsp_magnitude_qst_goal_signed_entry = h) /\ ((gsp_sign_qst_goal_signed_entry = 0 \/ gsp_sign_qst_goal_signed_entry = 1) /\ (((gsp_sign_qst_goal_signed_entry = 0 /\ (exists gsp_mod_left_qst_goal_signed_entry_lower gsp_mod_right_qst_goal_signed_entry_lower. (a * gsp_value_qst_goal_signed_entry) + p * gsp_mod_left_qst_goal_signed_entry_lower = (gsp_magnitude_qst_goal_signed_entry) + p * gsp_mod_right_qst_goal_signed_entry_lower)) \/ (gsp_sign_qst_goal_signed_entry = 1 /\ (exists gsp_mod_left_qst_goal_signed_entry_reflected gsp_mod_right_qst_goal_signed_entry_reflected. (a * gsp_value_qst_goal_signed_entry) + p * gsp_mod_left_qst_goal_signed_entry_reflected = ((2 * h) * gsp_magnitude_qst_goal_signed_entry) + p * gsp_mod_right_qst_goal_signed_entry_reflected))))))))))) -> (((exists ff_u_qst_goal_count_sum ff_v_qst_goal_count_sum. ((((exists ff_h_qst_goal_count_sum_start. ff_h_qst_goal_count_sum_start + S (0) = S ((S (0)) * ff_v_qst_goal_count_sum)) /\ exists ff_q_qst_goal_count_sum_start. ff_u_qst_goal_count_sum = ff_q_qst_goal_count_sum_start * S ((S (0)) * ff_v_qst_goal_count_sum) + (0))) /\ ((((exists ff_h_qst_goal_count_sum_terminal. ff_h_qst_goal_count_sum_terminal + S (e) = S ((S (h)) * ff_v_qst_goal_count_sum)) /\ exists ff_q_qst_goal_count_sum_terminal. ff_u_qst_goal_count_sum = ff_q_qst_goal_count_sum_terminal * S ((S (h)) * ff_v_qst_goal_count_sum) + (e))) /\ forall ff_i_qst_goal_count_sum. (exists ff_lt_qst_goal_count_sum_bound. ff_lt_qst_goal_count_sum_bound + S ff_i_qst_goal_count_sum = h) -> exists ff_a_qst_goal_count_sum ff_r_qst_goal_count_sum ff_s_qst_goal_count_sum. ((((exists ff_h_qst_goal_count_sum_summand. ff_h_qst_goal_count_sum_summand + S (ff_a_qst_goal_count_sum) = S ((S (ff_i_qst_goal_count_sum)) * sc)) /\ exists ff_q_qst_goal_count_sum_summand. sb = ff_q_qst_goal_count_sum_summand * S ((S (ff_i_qst_goal_count_sum)) * sc) + (ff_a_qst_goal_count_sum))) /\ ((((exists ff_h_qst_goal_count_sum_partial. ff_h_qst_goal_count_sum_partial + S (ff_r_qst_goal_count_sum) = S ((S (ff_i_qst_goal_count_sum)) * ff_v_qst_goal_count_sum)) /\ exists ff_q_qst_goal_count_sum_partial. ff_u_qst_goal_count_sum = ff_q_qst_goal_count_sum_partial * S ((S (ff_i_qst_goal_count_sum)) * ff_v_qst_goal_count_sum) + (ff_r_qst_goal_count_sum))) /\ ((((exists ff_h_qst_goal_count_sum_successor. ff_h_qst_goal_count_sum_successor + S (ff_s_qst_goal_count_sum) = S ((S (S ff_i_qst_goal_count_sum)) * ff_v_qst_goal_count_sum)) /\ exists ff_q_qst_goal_count_sum_successor. ff_u_qst_goal_count_sum = ff_q_qst_goal_count_sum_successor * S ((S (S ff_i_qst_goal_count_sum)) * ff_v_qst_goal_count_sum) + (ff_s_qst_goal_count_sum))) /\ ff_s_qst_goal_count_sum = ff_r_qst_goal_count_sum + ff_a_qst_goal_count_sum)))))) /\ (forall ff_i_qst_goal_count_bits. (exists ff_lt_qst_goal_count_bits_bound. ff_lt_qst_goal_count_bits_bound + S ff_i_qst_goal_count_bits = h) -> exists ff_bit_qst_goal_count_bits. ((((exists ff_h_qst_goal_count_bits_decoded. ff_h_qst_goal_count_bits_decoded + S (ff_bit_qst_goal_count_bits) = S ((S (ff_i_qst_goal_count_bits)) * sc)) /\ exists ff_q_qst_goal_count_bits_decoded. sb = ff_q_qst_goal_count_bits_decoded * S ((S (ff_i_qst_goal_count_bits)) * sc) + (ff_bit_qst_goal_count_bits))) /\ (ff_bit_qst_goal_count_bits = 0 \/ ff_bit_qst_goal_count_bits = 1))))) -> (((h = 2 * e) \/ (exists qst_count_half_goal. h = 2 * qst_count_half_goal + 1 /\ e = S qst_count_half_goal)))