double_quotient_carry_prefix_extend

Exact expanded PA statement

forall b c d e f g l. (forall b5cc_index_b5ccpe_before. (exists bcf_lt_gap_b5ccpe_before_bound. bcf_lt_gap_b5ccpe_before_bound + S (b5cc_index_b5ccpe_before) = l) -> exists b5cc_left_b5ccpe_before b5cc_right_b5ccpe_before b5cc_bit_b5ccpe_before. (((exists fs_h_b5cc_b5ccpe_before_left. fs_h_b5cc_b5ccpe_before_left + S (b5cc_left_b5ccpe_before) = S ((S (b5cc_index_b5ccpe_before)) * c)) /\ exists fs_q_b5cc_b5ccpe_before_left. b = fs_q_b5cc_b5ccpe_before_left * S ((S (b5cc_index_b5ccpe_before)) * c) + (b5cc_left_b5ccpe_before))) /\ ((((exists fs_h_b5cc_b5ccpe_before_right. fs_h_b5cc_b5ccpe_before_right + S (b5cc_right_b5ccpe_before) = S ((S (b5cc_index_b5ccpe_before)) * e)) /\ exists fs_q_b5cc_b5ccpe_before_right. d = fs_q_b5cc_b5ccpe_before_right * S ((S (b5cc_index_b5ccpe_before)) * e) + (b5cc_right_b5ccpe_before))) /\ ((((exists fs_h_b5cc_b5ccpe_before_bit. fs_h_b5cc_b5ccpe_before_bit + S (b5cc_bit_b5ccpe_before) = S ((S (b5cc_index_b5ccpe_before)) * g)) /\ exists fs_q_b5cc_b5ccpe_before_bit. f = fs_q_b5cc_b5ccpe_before_bit * S ((S (b5cc_index_b5ccpe_before)) * g) + (b5cc_bit_b5ccpe_before))) /\ (((b5cc_bit_b5ccpe_before = 0 /\ b5cc_right_b5ccpe_before = b5cc_left_b5ccpe_before + b5cc_left_b5ccpe_before) \/ (b5cc_bit_b5ccpe_before = 1 /\ b5cc_right_b5ccpe_before = S (b5cc_left_b5ccpe_before + b5cc_left_b5ccpe_before))))))) -> (exists q Q bit. (((exists fs_h_b5ccpe_last_left. fs_h_b5ccpe_last_left + S (q) = S ((S (l)) * c)) /\ exists fs_q_b5ccpe_last_left. b = fs_q_b5ccpe_last_left * S ((S (l)) * c) + (q))) /\ ((((exists fs_h_b5ccpe_last_right. fs_h_b5ccpe_last_right + S (Q) = S ((S (l)) * e)) /\ exists fs_q_b5ccpe_last_right. d = fs_q_b5ccpe_last_right * S ((S (l)) * e) + (Q))) /\ (((bit = 0 /\ Q = q + q) \/ (bit = 1 /\ Q = S (q + q)))))) -> exists z h. (forall b5cc_index_b5ccpe_after. (exists bcf_lt_gap_b5ccpe_after_bound. bcf_lt_gap_b5ccpe_after_bound + S (b5cc_index_b5ccpe_after) = S l) -> exists b5cc_left_b5ccpe_after b5cc_right_b5ccpe_after b5cc_bit_b5ccpe_after. (((exists fs_h_b5cc_b5ccpe_after_left. fs_h_b5cc_b5ccpe_after_left + S (b5cc_left_b5ccpe_after) = S ((S (b5cc_index_b5ccpe_after)) * c)) /\ exists fs_q_b5cc_b5ccpe_after_left. b = fs_q_b5cc_b5ccpe_after_left * S ((S (b5cc_index_b5ccpe_after)) * c) + (b5cc_left_b5ccpe_after))) /\ ((((exists fs_h_b5cc_b5ccpe_after_right. fs_h_b5cc_b5ccpe_after_right + S (b5cc_right_b5ccpe_after) = S ((S (b5cc_index_b5ccpe_after)) * e)) /\ exists fs_q_b5cc_b5ccpe_after_right. d = fs_q_b5cc_b5ccpe_after_right * S ((S (b5cc_index_b5ccpe_after)) * e) + (b5cc_right_b5ccpe_after))) /\ ((((exists fs_h_b5cc_b5ccpe_after_bit. fs_h_b5cc_b5ccpe_after_bit + S (b5cc_bit_b5ccpe_after) = S ((S (b5cc_index_b5ccpe_after)) * h)) /\ exists fs_q_b5cc_b5ccpe_after_bit. z = fs_q_b5cc_b5ccpe_after_bit * S ((S (b5cc_index_b5ccpe_after)) * h) + (b5cc_bit_b5ccpe_after))) /\ (((b5cc_bit_b5ccpe_after = 0 /\ b5cc_right_b5ccpe_after = b5cc_left_b5ccpe_after + b5cc_left_b5ccpe_after) \/ (b5cc_bit_b5ccpe_after = 1 /\ b5cc_right_b5ccpe_after = S (b5cc_left_b5ccpe_after + b5cc_left_b5ccpe_after)))))))