double_quotient_carry_prefix_all_bits

Exact expanded PA statement

forall b c d e f g l. (forall b5cc_index_b5ccpab_source. (exists bcf_lt_gap_b5ccpab_source_bound. bcf_lt_gap_b5ccpab_source_bound + S (b5cc_index_b5ccpab_source) = l) -> exists b5cc_left_b5ccpab_source b5cc_right_b5ccpab_source b5cc_bit_b5ccpab_source. (((exists fs_h_b5cc_b5ccpab_source_left. fs_h_b5cc_b5ccpab_source_left + S (b5cc_left_b5ccpab_source) = S ((S (b5cc_index_b5ccpab_source)) * c)) /\ exists fs_q_b5cc_b5ccpab_source_left. b = fs_q_b5cc_b5ccpab_source_left * S ((S (b5cc_index_b5ccpab_source)) * c) + (b5cc_left_b5ccpab_source))) /\ ((((exists fs_h_b5cc_b5ccpab_source_right. fs_h_b5cc_b5ccpab_source_right + S (b5cc_right_b5ccpab_source) = S ((S (b5cc_index_b5ccpab_source)) * e)) /\ exists fs_q_b5cc_b5ccpab_source_right. d = fs_q_b5cc_b5ccpab_source_right * S ((S (b5cc_index_b5ccpab_source)) * e) + (b5cc_right_b5ccpab_source))) /\ ((((exists fs_h_b5cc_b5ccpab_source_bit. fs_h_b5cc_b5ccpab_source_bit + S (b5cc_bit_b5ccpab_source) = S ((S (b5cc_index_b5ccpab_source)) * g)) /\ exists fs_q_b5cc_b5ccpab_source_bit. f = fs_q_b5cc_b5ccpab_source_bit * S ((S (b5cc_index_b5ccpab_source)) * g) + (b5cc_bit_b5ccpab_source))) /\ (((b5cc_bit_b5ccpab_source = 0 /\ b5cc_right_b5ccpab_source = b5cc_left_b5ccpab_source + b5cc_left_b5ccpab_source) \/ (b5cc_bit_b5ccpab_source = 1 /\ b5cc_right_b5ccpab_source = S (b5cc_left_b5ccpab_source + b5cc_left_b5ccpab_source))))))) -> (forall ff_i_b5ccpab_result. (exists ff_lt_b5ccpab_result_bound. ff_lt_b5ccpab_result_bound + S ff_i_b5ccpab_result = l) -> exists ff_bit_b5ccpab_result. ((((exists ff_h_b5ccpab_result_decoded. ff_h_b5ccpab_result_decoded + S (ff_bit_b5ccpab_result) = S ((S (ff_i_b5ccpab_result)) * g)) /\ exists ff_q_b5ccpab_result_decoded. f = ff_q_b5ccpab_result_decoded * S ((S (ff_i_b5ccpab_result)) * g) + (ff_bit_b5ccpab_result))) /\ (ff_bit_b5ccpab_result = 0 \/ ff_bit_b5ccpab_result = 1)))