prime_field_polynomial_add_from_normalization

forall p ab ac bb bc rb rc cb cc l. (forall fom_index_pfp_add_source_a. (exists fom_gap_pfp_add_source_a_index_bound. fom_gap_pfp_add_source_a_index_bound + S (fom_index_pfp_add_source_a) = l) -> exists fom_value_pfp_add_source_a. ((((exists fom_beta_height_pfp_add_source_a_entry. fom_beta_height_pfp_add_source_a_entry + S (fom_value_pfp_add_source_a) = S ((S (fom_index_pfp_add_source_a)) * ac)) /\ exists fom_beta_quotient_pfp_add_source_a_entry. ab = fom_beta_quotient_pfp_add_source_a_entry * S ((S (fom_index_pfp_add_source_a)) * ac) + (fom_value_pfp_add_source_a))) /\ (exists fom_gap_pfp_add_source_a_value_bound. fom_gap_pfp_add_source_a_value_bound + S (fom_value_pfp_add_source_a) = p))) -> (forall fom_index_pfp_add_source_b. (exists fom_gap_pfp_add_source_b_index_bound. fom_gap_pfp_add_source_b_index_bound + S (fom_index_pfp_add_source_b) = l) -> exists fom_value_pfp_add_source_b. ((((exists fom_beta_height_pfp_add_source_b_entry. fom_beta_height_pfp_add_source_b_entry + S (fom_value_pfp_add_source_b) = S ((S (fom_index_pfp_add_source_b)) * bc)) /\ exists fom_beta_quotient_pfp_add_source_b_entry. bb = fom_beta_quotient_pfp_add_source_b_entry * S ((S (fom_index_pfp_add_source_b)) * bc) + (fom_value_pfp_add_source_b))) /\ (exists fom_gap_pfp_add_source_b_value_bound. fom_gap_pfp_add_source_b_value_bound + S (fom_value_pfp_add_source_b) = p))) -> (forall ff_index_mcp_add_pfp_add_raw ff_left_mcp_add_pfp_add_raw ff_right_mcp_add_pfp_add_raw ff_target_mcp_add_pfp_add_raw. (exists mcp_gap_pfp_add_raw_bound. mcp_gap_pfp_add_raw_bound + S (ff_index_mcp_add_pfp_add_raw) = (l)) -> (((exists fs_h_mcp_pfp_add_raw_left. fs_h_mcp_pfp_add_raw_left + S (ff_left_mcp_add_pfp_add_raw) = S ((S (ff_index_mcp_add_pfp_add_raw)) * ac)) /\ exists fs_q_mcp_pfp_add_raw_left. ab = fs_q_mcp_pfp_add_raw_left * S ((S (ff_index_mcp_add_pfp_add_raw)) * ac) + (ff_left_mcp_add_pfp_add_raw))) -> (((exists fs_h_mcp_pfp_add_raw_right. fs_h_mcp_pfp_add_raw_right + S (ff_right_mcp_add_pfp_add_raw) = S ((S (ff_index_mcp_add_pfp_add_raw)) * bc)) /\ exists fs_q_mcp_pfp_add_raw_right. bb = fs_q_mcp_pfp_add_raw_right * S ((S (ff_index_mcp_add_pfp_add_raw)) * bc) + (ff_right_mcp_add_pfp_add_raw))) -> (((exists fs_h_mcp_pfp_add_raw_target. fs_h_mcp_pfp_add_raw_target + S (ff_target_mcp_add_pfp_add_raw) = S ((S (ff_index_mcp_add_pfp_add_raw)) * rc)) /\ exists fs_q_mcp_pfp_add_raw_target. rb = fs_q_mcp_pfp_add_raw_target * S ((S (ff_index_mcp_add_pfp_add_raw)) * rc) + (ff_target_mcp_add_pfp_add_raw))) -> ff_target_mcp_add_pfp_add_raw = ff_left_mcp_add_pfp_add_raw + ff_right_mcp_add_pfp_add_raw) -> (forall pfp_index_add_normalize. (exists pfa_gap_add_normalizeindex. pfa_gap_add_normalizeindex + S (pfp_index_add_normalize) = (l)) -> exists pfp_source_add_normalize pfp_residue_add_normalize. ((((exists ff_h_pfp_add_normalizesource. ff_h_pfp_add_normalizesource + S (pfp_source_add_normalize) = S ((S (pfp_index_add_normalize)) * rc)) /\ exists ff_q_pfp_add_normalizesource. rb = ff_q_pfp_add_normalizesource * S ((S (pfp_index_add_normalize)) * rc) + (pfp_source_add_normalize))) /\ (((((exists ff_h_pfp_add_normalizetarget. ff_h_pfp_add_normalizetarget + S (pfp_residue_add_normalize) = S ((S (pfp_index_add_normalize)) * cc)) /\ exists ff_q_pfp_add_normalizetarget. cb = ff_q_pfp_add_normalizetarget * S ((S (pfp_index_add_normalize)) * cc) + (pfp_residue_add_normalize))) /\ ((((exists pfa_gap_add_normalizeresiduebound. pfa_gap_add_normalizeresiduebound + S (pfp_residue_add_normalize) = (p)) /\ ((exists pfa_offset_left_add_normalizeresiduecongruence pfa_offset_right_add_normalizeresiduecongruence. (pfp_source_add_normalize) + (p) * pfa_offset_left_add_normalizeresiduecongruence = (pfp_residue_add_normalize) + (p) * pfa_offset_right_add_normalizeresiduecongruence))))))))) -> (forall pfp_index_add_result. (exists pfa_gap_add_resultindex. pfa_gap_add_resultindex + S (pfp_index_add_result) = (l)) -> exists pfp_left_add_result pfp_right_add_result pfp_value_add_result. ((((exists ff_h_pfp_add_resultleft. ff_h_pfp_add_resultleft + S (pfp_left_add_result) = S ((S (pfp_index_add_result)) * ac)) /\ exists ff_q_pfp_add_resultleft. ab = ff_q_pfp_add_resultleft * S ((S (pfp_index_add_result)) * ac) + (pfp_left_add_result))) /\ (((((exists ff_h_pfp_add_resultright. ff_h_pfp_add_resultright + S (pfp_right_add_result) = S ((S (pfp_index_add_result)) * bc)) /\ exists ff_q_pfp_add_resultright. bb = ff_q_pfp_add_resultright * S ((S (pfp_index_add_result)) * bc) + (pfp_right_add_result))) /\ (((((exists ff_h_pfp_add_resulttarget. ff_h_pfp_add_resulttarget + S (pfp_value_add_result) = S ((S (pfp_index_add_result)) * cc)) /\ exists ff_q_pfp_add_resulttarget. cb = ff_q_pfp_add_resulttarget * S ((S (pfp_index_add_result)) * cc) + (pfp_value_add_result))) /\ ((((exists pfa_gap_add_resultoperationleft. pfa_gap_add_resultoperationleft + S (pfp_left_add_result) = (p)) /\ (((exists pfa_gap_add_resultoperationright. pfa_gap_add_resultoperationright + S (pfp_right_add_result) = (p)) /\ ((((exists pfa_gap_add_resultoperationresultbound. pfa_gap_add_resultoperationresultbound + S (pfp_value_add_result) = (p)) /\ ((exists pfa_offset_left_add_resultoperationresultcongruence pfa_offset_right_add_resultoperationresultcongruence. ((pfp_left_add_result) + (pfp_right_add_result)) + (p) * pfa_offset_left_add_resultoperationresultcongruence = (pfp_value_add_result) + (p) * pfa_offset_right_add_resultoperationresultcongruence))))))))))))))))