gauss_signed_half_bit_count_exists

Exact expanded PA statement

forall p h a b c mb mc sb sc l. (forall gsp_index_count_source. (exists gsp_lt_gap_count_source_index_bound. gsp_lt_gap_count_source_index_bound + S gsp_index_count_source = l) -> (exists gsp_value_count_source_entry gsp_magnitude_count_source_entry gsp_sign_count_source_entry. (((exists ff_h_gsp_count_source_entry_source. ff_h_gsp_count_source_entry_source + S (gsp_value_count_source_entry) = S ((S (gsp_index_count_source)) * c)) /\ exists ff_q_gsp_count_source_entry_source. b = ff_q_gsp_count_source_entry_source * S ((S (gsp_index_count_source)) * c) + (gsp_value_count_source_entry))) /\ ((((exists ff_h_gsp_count_source_entry_magnitude. ff_h_gsp_count_source_entry_magnitude + S (gsp_magnitude_count_source_entry) = S ((S (gsp_index_count_source)) * mc)) /\ exists ff_q_gsp_count_source_entry_magnitude. mb = ff_q_gsp_count_source_entry_magnitude * S ((S (gsp_index_count_source)) * mc) + (gsp_magnitude_count_source_entry))) /\ ((((exists ff_h_gsp_count_source_entry_sign. ff_h_gsp_count_source_entry_sign + S (gsp_sign_count_source_entry) = S ((S (gsp_index_count_source)) * sc)) /\ exists ff_q_gsp_count_source_entry_sign. sb = ff_q_gsp_count_source_entry_sign * S ((S (gsp_index_count_source)) * sc) + (gsp_sign_count_source_entry))) /\ ((exists gsp_lt_gap_count_source_entry_positive. gsp_lt_gap_count_source_entry_positive + S 0 = gsp_magnitude_count_source_entry) /\ ((exists gsp_le_gap_count_source_entry_bounded. gsp_le_gap_count_source_entry_bounded + gsp_magnitude_count_source_entry = h) /\ ((gsp_sign_count_source_entry = 0 \/ gsp_sign_count_source_entry = 1) /\ (((gsp_sign_count_source_entry = 0 /\ (exists gsp_mod_left_count_source_entry_lower gsp_mod_right_count_source_entry_lower. (a * gsp_value_count_source_entry) + p * gsp_mod_left_count_source_entry_lower = (gsp_magnitude_count_source_entry) + p * gsp_mod_right_count_source_entry_lower)) \/ (gsp_sign_count_source_entry = 1 /\ (exists gsp_mod_left_count_source_entry_reflected gsp_mod_right_count_source_entry_reflected. (a * gsp_value_count_source_entry) + p * gsp_mod_left_count_source_entry_reflected = ((2 * h) * gsp_magnitude_count_source_entry) + p * gsp_mod_right_count_source_entry_reflected))))))))))) -> exists n. (((exists ff_u_gsp_count_result_sum ff_v_gsp_count_result_sum. ((((exists ff_h_gsp_count_result_sum_start. ff_h_gsp_count_result_sum_start + S (0) = S ((S (0)) * ff_v_gsp_count_result_sum)) /\ exists ff_q_gsp_count_result_sum_start. ff_u_gsp_count_result_sum = ff_q_gsp_count_result_sum_start * S ((S (0)) * ff_v_gsp_count_result_sum) + (0))) /\ ((((exists ff_h_gsp_count_result_sum_terminal. ff_h_gsp_count_result_sum_terminal + S (n) = S ((S (l)) * ff_v_gsp_count_result_sum)) /\ exists ff_q_gsp_count_result_sum_terminal. ff_u_gsp_count_result_sum = ff_q_gsp_count_result_sum_terminal * S ((S (l)) * ff_v_gsp_count_result_sum) + (n))) /\ forall ff_i_gsp_count_result_sum. (exists ff_lt_gsp_count_result_sum_bound. ff_lt_gsp_count_result_sum_bound + S ff_i_gsp_count_result_sum = l) -> exists ff_a_gsp_count_result_sum ff_r_gsp_count_result_sum ff_s_gsp_count_result_sum. ((((exists ff_h_gsp_count_result_sum_summand. ff_h_gsp_count_result_sum_summand + S (ff_a_gsp_count_result_sum) = S ((S (ff_i_gsp_count_result_sum)) * sc)) /\ exists ff_q_gsp_count_result_sum_summand. sb = ff_q_gsp_count_result_sum_summand * S ((S (ff_i_gsp_count_result_sum)) * sc) + (ff_a_gsp_count_result_sum))) /\ ((((exists ff_h_gsp_count_result_sum_partial. ff_h_gsp_count_result_sum_partial + S (ff_r_gsp_count_result_sum) = S ((S (ff_i_gsp_count_result_sum)) * ff_v_gsp_count_result_sum)) /\ exists ff_q_gsp_count_result_sum_partial. ff_u_gsp_count_result_sum = ff_q_gsp_count_result_sum_partial * S ((S (ff_i_gsp_count_result_sum)) * ff_v_gsp_count_result_sum) + (ff_r_gsp_count_result_sum))) /\ ((((exists ff_h_gsp_count_result_sum_successor. ff_h_gsp_count_result_sum_successor + S (ff_s_gsp_count_result_sum) = S ((S (S ff_i_gsp_count_result_sum)) * ff_v_gsp_count_result_sum)) /\ exists ff_q_gsp_count_result_sum_successor. ff_u_gsp_count_result_sum = ff_q_gsp_count_result_sum_successor * S ((S (S ff_i_gsp_count_result_sum)) * ff_v_gsp_count_result_sum) + (ff_s_gsp_count_result_sum))) /\ ff_s_gsp_count_result_sum = ff_r_gsp_count_result_sum + ff_a_gsp_count_result_sum)))))) /\ (forall ff_i_gsp_count_result_bits. (exists ff_lt_gsp_count_result_bits_bound. ff_lt_gsp_count_result_bits_bound + S ff_i_gsp_count_result_bits = l) -> exists ff_bit_gsp_count_result_bits. ((((exists ff_h_gsp_count_result_bits_decoded. ff_h_gsp_count_result_bits_decoded + S (ff_bit_gsp_count_result_bits) = S ((S (ff_i_gsp_count_result_bits)) * sc)) /\ exists ff_q_gsp_count_result_bits_decoded. sb = ff_q_gsp_count_result_bits_decoded * S ((S (ff_i_gsp_count_result_bits)) * sc) + (ff_bit_gsp_count_result_bits))) /\ (ff_bit_gsp_count_result_bits = 0 \/ ff_bit_gsp_count_result_bits = 1)))))