double_quotient_carry_prefix_restrict

Exact expanded PA statement

forall b c d e f g l. (forall b5cc_index_b5ccpr_source. (exists bcf_lt_gap_b5ccpr_source_bound. bcf_lt_gap_b5ccpr_source_bound + S (b5cc_index_b5ccpr_source) = S l) -> exists b5cc_left_b5ccpr_source b5cc_right_b5ccpr_source b5cc_bit_b5ccpr_source. (((exists fs_h_b5cc_b5ccpr_source_left. fs_h_b5cc_b5ccpr_source_left + S (b5cc_left_b5ccpr_source) = S ((S (b5cc_index_b5ccpr_source)) * c)) /\ exists fs_q_b5cc_b5ccpr_source_left. b = fs_q_b5cc_b5ccpr_source_left * S ((S (b5cc_index_b5ccpr_source)) * c) + (b5cc_left_b5ccpr_source))) /\ ((((exists fs_h_b5cc_b5ccpr_source_right. fs_h_b5cc_b5ccpr_source_right + S (b5cc_right_b5ccpr_source) = S ((S (b5cc_index_b5ccpr_source)) * e)) /\ exists fs_q_b5cc_b5ccpr_source_right. d = fs_q_b5cc_b5ccpr_source_right * S ((S (b5cc_index_b5ccpr_source)) * e) + (b5cc_right_b5ccpr_source))) /\ ((((exists fs_h_b5cc_b5ccpr_source_bit. fs_h_b5cc_b5ccpr_source_bit + S (b5cc_bit_b5ccpr_source) = S ((S (b5cc_index_b5ccpr_source)) * g)) /\ exists fs_q_b5cc_b5ccpr_source_bit. f = fs_q_b5cc_b5ccpr_source_bit * S ((S (b5cc_index_b5ccpr_source)) * g) + (b5cc_bit_b5ccpr_source))) /\ (((b5cc_bit_b5ccpr_source = 0 /\ b5cc_right_b5ccpr_source = b5cc_left_b5ccpr_source + b5cc_left_b5ccpr_source) \/ (b5cc_bit_b5ccpr_source = 1 /\ b5cc_right_b5ccpr_source = S (b5cc_left_b5ccpr_source + b5cc_left_b5ccpr_source))))))) -> (forall b5cc_index_b5ccpr_result. (exists bcf_lt_gap_b5ccpr_result_bound. bcf_lt_gap_b5ccpr_result_bound + S (b5cc_index_b5ccpr_result) = l) -> exists b5cc_left_b5ccpr_result b5cc_right_b5ccpr_result b5cc_bit_b5ccpr_result. (((exists fs_h_b5cc_b5ccpr_result_left. fs_h_b5cc_b5ccpr_result_left + S (b5cc_left_b5ccpr_result) = S ((S (b5cc_index_b5ccpr_result)) * c)) /\ exists fs_q_b5cc_b5ccpr_result_left. b = fs_q_b5cc_b5ccpr_result_left * S ((S (b5cc_index_b5ccpr_result)) * c) + (b5cc_left_b5ccpr_result))) /\ ((((exists fs_h_b5cc_b5ccpr_result_right. fs_h_b5cc_b5ccpr_result_right + S (b5cc_right_b5ccpr_result) = S ((S (b5cc_index_b5ccpr_result)) * e)) /\ exists fs_q_b5cc_b5ccpr_result_right. d = fs_q_b5cc_b5ccpr_result_right * S ((S (b5cc_index_b5ccpr_result)) * e) + (b5cc_right_b5ccpr_result))) /\ ((((exists fs_h_b5cc_b5ccpr_result_bit. fs_h_b5cc_b5ccpr_result_bit + S (b5cc_bit_b5ccpr_result) = S ((S (b5cc_index_b5ccpr_result)) * g)) /\ exists fs_q_b5cc_b5ccpr_result_bit. f = fs_q_b5cc_b5ccpr_result_bit * S ((S (b5cc_index_b5ccpr_result)) * g) + (b5cc_bit_b5ccpr_result))) /\ (((b5cc_bit_b5ccpr_result = 0 /\ b5cc_right_b5ccpr_result = b5cc_left_b5ccpr_result + b5cc_left_b5ccpr_result) \/ (b5cc_bit_b5ccpr_result = 1 /\ b5cc_right_b5ccpr_result = S (b5cc_left_b5ccpr_result + b5cc_left_b5ccpr_result)))))))