prime_field_polynomial_quotient_prefix_remainder_zero

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc d qb qc N b pb pc L ub uc. (~((p) = 1) /\ forall pfa_factor_left_division_zero_prime pfa_factor_right_division_zero_prime. (p) = pfa_factor_left_division_zero_prime * pfa_factor_right_division_zero_prime -> pfa_factor_left_division_zero_prime = 1 \/ pfa_factor_right_division_zero_prime = 1) -> (((exists ff_h_pfp_division_zero_head. ff_h_pfp_division_zero_head + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_zero_head. bb = ff_q_pfp_division_zero_head * S ((S (0)) * bc) + (b))) -> (((~((b) = 0)) /\ ((((exists pfa_gap_division_zero_inversemultiplicationleft. pfa_gap_division_zero_inversemultiplicationleft + S (b) = (p)) /\ (((exists pfa_gap_division_zero_inversemultiplicationright. pfa_gap_division_zero_inversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_division_zero_inversemultiplicationresultbound. pfa_gap_division_zero_inversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_zero_inversemultiplicationresultcongruence pfa_offset_right_division_zero_inversemultiplicationresultcongruence. ((b) * (k)) + (p) * pfa_offset_left_division_zero_inversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_zero_inversemultiplicationresultcongruence)))))))))))) -> (forall pfd_index_division_zero_execution. (exists pfa_gap_division_zero_executionbound. pfa_gap_division_zero_executionbound + S (pfd_index_division_zero_execution) = (N)) -> exists pfd_value_division_zero_execution. ((((exists ff_h_pfp_division_zero_executionentry. ff_h_pfp_division_zero_executionentry + S (pfd_value_division_zero_execution) = S ((S (pfd_index_division_zero_execution)) * qc)) /\ exists ff_q_pfp_division_zero_executionentry. qb = ff_q_pfp_division_zero_executionentry * S ((S (pfd_index_division_zero_execution)) * qc) + (pfd_value_division_zero_execution))) /\ ((exists pfd_input_division_zero_executionstep pfd_previous_division_zero_executionstep pfd_difference_division_zero_executionstep. ((((exists ff_h_pfp_division_zero_executionstepinput. ff_h_pfp_division_zero_executionstepinput + S (pfd_input_division_zero_executionstep) = S ((S (pfd_index_division_zero_execution)) * ac)) /\ exists ff_q_pfp_division_zero_executionstepinput. ab = ff_q_pfp_division_zero_executionstepinput * S ((S (pfd_index_division_zero_execution)) * ac) + (pfd_input_division_zero_executionstep))) /\ (((exists pfc_terms_code_division_zero_executionstepprevious pfc_terms_scale_division_zero_executionstepprevious pfc_natural_sum_division_zero_executionstepprevious. ((forall pfc_index_division_zero_executionsteppreviousdiagonal. (exists pfa_gap_division_zero_executionsteppreviousdiagonalbound. pfa_gap_division_zero_executionsteppreviousdiagonalbound + S (pfc_index_division_zero_executionsteppreviousdiagonal) = (S (pfd_index_division_zero_execution))) -> exists pfc_value_division_zero_executionsteppreviousdiagonal. ((((exists ff_h_pfp_division_zero_executionsteppreviousdiagonalentry. ff_h_pfp_division_zero_executionsteppreviousdiagonalentry + S (pfc_value_division_zero_executionsteppreviousdiagonal) = S ((S (pfc_index_division_zero_executionsteppreviousdiagonal)) * pfc_terms_scale_division_zero_executionstepprevious)) /\ exists ff_q_pfp_division_zero_executionsteppreviousdiagonalentry. pfc_terms_code_division_zero_executionstepprevious = ff_q_pfp_division_zero_executionsteppreviousdiagonalentry * S ((S (pfc_index_division_zero_executionsteppreviousdiagonal)) * pfc_terms_scale_division_zero_executionstepprevious) + (pfc_value_division_zero_executionsteppreviousdiagonal))) /\ ((exists pfc_complement_division_zero_executionsteppreviousdiagonalterm pfc_left_division_zero_executionsteppreviousdiagonalterm pfc_right_division_zero_executionsteppreviousdiagonalterm. (((pfc_index_division_zero_executionsteppreviousdiagonal)+pfc_complement_division_zero_executionsteppreviousdiagonalterm=(pfd_index_division_zero_execution)) /\ ((((((exists pfa_gap_division_zero_executionsteppreviousdiagonaltermleftinside. pfa_gap_division_zero_executionsteppreviousdiagonaltermleftinside + S (pfc_index_division_zero_executionsteppreviousdiagonal) = (pfd_index_division_zero_execution)) /\ ((((exists ff_h_pfp_division_zero_executionsteppreviousdiagonaltermleftentry. ff_h_pfp_division_zero_executionsteppreviousdiagonaltermleftentry + S (pfc_left_division_zero_executionsteppreviousdiagonalterm) = S ((S (pfc_index_division_zero_executionsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_zero_executionsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_zero_executionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_zero_executionsteppreviousdiagonal)) * qc) + (pfc_left_division_zero_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_zero_executionsteppreviousdiagonaltermleftoutside. pfc_gap_division_zero_executionsteppreviousdiagonaltermleftoutside+(pfd_index_division_zero_execution)=(pfc_index_division_zero_executionsteppreviousdiagonal)) /\ (((pfc_left_division_zero_executionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_zero_executionsteppreviousdiagonaltermrightinside. pfa_gap_division_zero_executionsteppreviousdiagonaltermrightinside + S (pfc_complement_division_zero_executionsteppreviousdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_zero_executionsteppreviousdiagonaltermrightentry. ff_h_pfp_division_zero_executionsteppreviousdiagonaltermrightentry + S (pfc_right_division_zero_executionsteppreviousdiagonalterm) = S ((S (pfc_complement_division_zero_executionsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_zero_executionsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_zero_executionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_zero_executionsteppreviousdiagonalterm)) * bc) + (pfc_right_division_zero_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_zero_executionsteppreviousdiagonaltermrightoutside. pfc_gap_division_zero_executionsteppreviousdiagonaltermrightoutside+(S d)=(pfc_complement_division_zero_executionsteppreviousdiagonalterm)) /\ (((pfc_right_division_zero_executionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_zero_executionsteppreviousdiagonal)=pfc_left_division_zero_executionsteppreviousdiagonalterm*pfc_right_division_zero_executionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_zero_executionstepprevioussum fs_v_pfc_division_zero_executionstepprevioussum. ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_start. fs_h_pfc_division_zero_executionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_zero_executionstepprevioussum)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_start. fs_u_pfc_division_zero_executionstepprevioussum = fs_q_pfc_division_zero_executionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_zero_executionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_terminal. fs_h_pfc_division_zero_executionstepprevioussum_body_terminal + S (pfc_natural_sum_division_zero_executionstepprevious) = S ((S (S (pfd_index_division_zero_execution))) * fs_v_pfc_division_zero_executionstepprevioussum)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_terminal. fs_u_pfc_division_zero_executionstepprevioussum = fs_q_pfc_division_zero_executionstepprevioussum_body_terminal * S ((S (S (pfd_index_division_zero_execution))) * fs_v_pfc_division_zero_executionstepprevioussum) + (pfc_natural_sum_division_zero_executionstepprevious))) /\ forall fs_i_pfc_division_zero_executionstepprevioussum_body_steps. (exists fs_lt_pfc_division_zero_executionstepprevioussum_body_steps_bound. fs_lt_pfc_division_zero_executionstepprevioussum_body_steps_bound + S fs_i_pfc_division_zero_executionstepprevioussum_body_steps = S (pfd_index_division_zero_execution)) -> exists fs_a_pfc_division_zero_executionstepprevioussum_body_steps fs_r_pfc_division_zero_executionstepprevioussum_body_steps fs_s_pfc_division_zero_executionstepprevioussum_body_steps. ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_steps_summand. fs_h_pfc_division_zero_executionstepprevioussum_body_steps_summand + S (fs_a_pfc_division_zero_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_zero_executionstepprevious)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_steps_summand. pfc_terms_code_division_zero_executionstepprevious = fs_q_pfc_division_zero_executionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_zero_executionstepprevious) + (fs_a_pfc_division_zero_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_steps_partial. fs_h_pfc_division_zero_executionstepprevioussum_body_steps_partial + S (fs_r_pfc_division_zero_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * fs_v_pfc_division_zero_executionstepprevioussum)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_steps_partial. fs_u_pfc_division_zero_executionstepprevioussum = fs_q_pfc_division_zero_executionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * fs_v_pfc_division_zero_executionstepprevioussum) + (fs_r_pfc_division_zero_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_steps_successor. fs_h_pfc_division_zero_executionstepprevioussum_body_steps_successor + S (fs_s_pfc_division_zero_executionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * fs_v_pfc_division_zero_executionstepprevioussum)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_steps_successor. fs_u_pfc_division_zero_executionstepprevioussum = fs_q_pfc_division_zero_executionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * fs_v_pfc_division_zero_executionstepprevioussum) + (fs_s_pfc_division_zero_executionstepprevioussum_body_steps))) /\ fs_s_pfc_division_zero_executionstepprevioussum_body_steps = fs_r_pfc_division_zero_executionstepprevioussum_body_steps + fs_a_pfc_division_zero_executionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_zero_executionsteppreviousresiduebound. pfa_gap_division_zero_executionsteppreviousresiduebound + S (pfd_previous_division_zero_executionstep) = (p)) /\ ((exists pfa_offset_left_division_zero_executionsteppreviousresiduecongruence pfa_offset_right_division_zero_executionsteppreviousresiduecongruence. (pfc_natural_sum_division_zero_executionstepprevious) + (p) * pfa_offset_left_division_zero_executionsteppreviousresiduecongruence = (pfd_previous_division_zero_executionstep) + (p) * pfa_offset_right_division_zero_executionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_zero_executionstepsubtractleft. pfa_gap_division_zero_executionstepsubtractleft + S (pfd_previous_division_zero_executionstep) = (p)) /\ (((exists pfa_gap_division_zero_executionstepsubtractright. pfa_gap_division_zero_executionstepsubtractright + S (pfd_difference_division_zero_executionstep) = (p)) /\ ((((exists pfa_gap_division_zero_executionstepsubtractresultbound. pfa_gap_division_zero_executionstepsubtractresultbound + S (pfd_input_division_zero_executionstep) = (p)) /\ ((exists pfa_offset_left_division_zero_executionstepsubtractresultcongruence pfa_offset_right_division_zero_executionstepsubtractresultcongruence. ((pfd_previous_division_zero_executionstep) + (pfd_difference_division_zero_executionstep)) + (p) * pfa_offset_left_division_zero_executionstepsubtractresultcongruence = (pfd_input_division_zero_executionstep) + (p) * pfa_offset_right_division_zero_executionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_zero_executionstepmultiplyleft. pfa_gap_division_zero_executionstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_zero_executionstepmultiplyright. pfa_gap_division_zero_executionstepmultiplyright + S (pfd_difference_division_zero_executionstep) = (p)) /\ ((((exists pfa_gap_division_zero_executionstepmultiplyresultbound. pfa_gap_division_zero_executionstepmultiplyresultbound + S (pfd_value_division_zero_execution) = (p)) /\ ((exists pfa_offset_left_division_zero_executionstepmultiplyresultcongruence pfa_offset_right_division_zero_executionstepmultiplyresultcongruence. ((k) * (pfd_difference_division_zero_executionstep)) + (p) * pfa_offset_left_division_zero_executionstepmultiplyresultcongruence = (pfd_value_division_zero_execution) + (p) * pfa_offset_right_division_zero_executionstepmultiplyresultcongruence))))))))))))))))))) -> (exists pfc_gap_division_zero_length. pfc_gap_division_zero_length+(N)=(L)) -> (forall pfc_index_division_zero_product. (exists pfa_gap_division_zero_productbound. pfa_gap_division_zero_productbound + S (pfc_index_division_zero_product) = (L)) -> exists pfc_value_division_zero_product. ((((exists ff_h_pfp_division_zero_productentry. ff_h_pfp_division_zero_productentry + S (pfc_value_division_zero_product) = S ((S (pfc_index_division_zero_product)) * pc)) /\ exists ff_q_pfp_division_zero_productentry. pb = ff_q_pfp_division_zero_productentry * S ((S (pfc_index_division_zero_product)) * pc) + (pfc_value_division_zero_product))) /\ ((exists pfc_terms_code_division_zero_productcoefficient pfc_terms_scale_division_zero_productcoefficient pfc_natural_sum_division_zero_productcoefficient. ((forall pfc_index_division_zero_productcoefficientdiagonal. (exists pfa_gap_division_zero_productcoefficientdiagonalbound. pfa_gap_division_zero_productcoefficientdiagonalbound + S (pfc_index_division_zero_productcoefficientdiagonal) = (S (pfc_index_division_zero_product))) -> exists pfc_value_division_zero_productcoefficientdiagonal. ((((exists ff_h_pfp_division_zero_productcoefficientdiagonalentry. ff_h_pfp_division_zero_productcoefficientdiagonalentry + S (pfc_value_division_zero_productcoefficientdiagonal) = S ((S (pfc_index_division_zero_productcoefficientdiagonal)) * pfc_terms_scale_division_zero_productcoefficient)) /\ exists ff_q_pfp_division_zero_productcoefficientdiagonalentry. pfc_terms_code_division_zero_productcoefficient = ff_q_pfp_division_zero_productcoefficientdiagonalentry * S ((S (pfc_index_division_zero_productcoefficientdiagonal)) * pfc_terms_scale_division_zero_productcoefficient) + (pfc_value_division_zero_productcoefficientdiagonal))) /\ ((exists pfc_complement_division_zero_productcoefficientdiagonalterm pfc_left_division_zero_productcoefficientdiagonalterm pfc_right_division_zero_productcoefficientdiagonalterm. (((pfc_index_division_zero_productcoefficientdiagonal)+pfc_complement_division_zero_productcoefficientdiagonalterm=(pfc_index_division_zero_product)) /\ ((((((exists pfa_gap_division_zero_productcoefficientdiagonaltermleftinside. pfa_gap_division_zero_productcoefficientdiagonaltermleftinside + S (pfc_index_division_zero_productcoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_division_zero_productcoefficientdiagonaltermleftentry. ff_h_pfp_division_zero_productcoefficientdiagonaltermleftentry + S (pfc_left_division_zero_productcoefficientdiagonalterm) = S ((S (pfc_index_division_zero_productcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_zero_productcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_zero_productcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_zero_productcoefficientdiagonal)) * qc) + (pfc_left_division_zero_productcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_zero_productcoefficientdiagonaltermleftoutside. pfc_gap_division_zero_productcoefficientdiagonaltermleftoutside+(N)=(pfc_index_division_zero_productcoefficientdiagonal)) /\ (((pfc_left_division_zero_productcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_zero_productcoefficientdiagonaltermrightinside. pfa_gap_division_zero_productcoefficientdiagonaltermrightinside + S (pfc_complement_division_zero_productcoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_zero_productcoefficientdiagonaltermrightentry. ff_h_pfp_division_zero_productcoefficientdiagonaltermrightentry + S (pfc_right_division_zero_productcoefficientdiagonalterm) = S ((S (pfc_complement_division_zero_productcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_zero_productcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_zero_productcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_zero_productcoefficientdiagonalterm)) * bc) + (pfc_right_division_zero_productcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_zero_productcoefficientdiagonaltermrightoutside. pfc_gap_division_zero_productcoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_division_zero_productcoefficientdiagonalterm)) /\ (((pfc_right_division_zero_productcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_zero_productcoefficientdiagonal)=pfc_left_division_zero_productcoefficientdiagonalterm*pfc_right_division_zero_productcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_zero_productcoefficientsum fs_v_pfc_division_zero_productcoefficientsum. ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_start. fs_h_pfc_division_zero_productcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_zero_productcoefficientsum)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_start. fs_u_pfc_division_zero_productcoefficientsum = fs_q_pfc_division_zero_productcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_zero_productcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_terminal. fs_h_pfc_division_zero_productcoefficientsum_body_terminal + S (pfc_natural_sum_division_zero_productcoefficient) = S ((S (S (pfc_index_division_zero_product))) * fs_v_pfc_division_zero_productcoefficientsum)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_terminal. fs_u_pfc_division_zero_productcoefficientsum = fs_q_pfc_division_zero_productcoefficientsum_body_terminal * S ((S (S (pfc_index_division_zero_product))) * fs_v_pfc_division_zero_productcoefficientsum) + (pfc_natural_sum_division_zero_productcoefficient))) /\ forall fs_i_pfc_division_zero_productcoefficientsum_body_steps. (exists fs_lt_pfc_division_zero_productcoefficientsum_body_steps_bound. fs_lt_pfc_division_zero_productcoefficientsum_body_steps_bound + S fs_i_pfc_division_zero_productcoefficientsum_body_steps = S (pfc_index_division_zero_product)) -> exists fs_a_pfc_division_zero_productcoefficientsum_body_steps fs_r_pfc_division_zero_productcoefficientsum_body_steps fs_s_pfc_division_zero_productcoefficientsum_body_steps. ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_steps_summand. fs_h_pfc_division_zero_productcoefficientsum_body_steps_summand + S (fs_a_pfc_division_zero_productcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * pfc_terms_scale_division_zero_productcoefficient)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_steps_summand. pfc_terms_code_division_zero_productcoefficient = fs_q_pfc_division_zero_productcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * pfc_terms_scale_division_zero_productcoefficient) + (fs_a_pfc_division_zero_productcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_steps_partial. fs_h_pfc_division_zero_productcoefficientsum_body_steps_partial + S (fs_r_pfc_division_zero_productcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * fs_v_pfc_division_zero_productcoefficientsum)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_steps_partial. fs_u_pfc_division_zero_productcoefficientsum = fs_q_pfc_division_zero_productcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * fs_v_pfc_division_zero_productcoefficientsum) + (fs_r_pfc_division_zero_productcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_steps_successor. fs_h_pfc_division_zero_productcoefficientsum_body_steps_successor + S (fs_s_pfc_division_zero_productcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * fs_v_pfc_division_zero_productcoefficientsum)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_steps_successor. fs_u_pfc_division_zero_productcoefficientsum = fs_q_pfc_division_zero_productcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * fs_v_pfc_division_zero_productcoefficientsum) + (fs_s_pfc_division_zero_productcoefficientsum_body_steps))) /\ fs_s_pfc_division_zero_productcoefficientsum_body_steps = fs_r_pfc_division_zero_productcoefficientsum_body_steps + fs_a_pfc_division_zero_productcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_zero_productcoefficientresiduebound. pfa_gap_division_zero_productcoefficientresiduebound + S (pfc_value_division_zero_product) = (p)) /\ ((exists pfa_offset_left_division_zero_productcoefficientresiduecongruence pfa_offset_right_division_zero_productcoefficientresiduecongruence. (pfc_natural_sum_division_zero_productcoefficient) + (p) * pfa_offset_left_division_zero_productcoefficientresiduecongruence = (pfc_value_division_zero_product) + (p) * pfa_offset_right_division_zero_productcoefficientresiduecongruence)))))))))))) -> (forall pfs_index_division_zero_subtraction. (exists pfa_gap_division_zero_subtractionindex. pfa_gap_division_zero_subtractionindex + S (pfs_index_division_zero_subtraction) = (L)) -> exists pfs_left_division_zero_subtraction pfs_right_division_zero_subtraction pfs_result_division_zero_subtraction. ((((exists ff_h_pfp_division_zero_subtractionleft. ff_h_pfp_division_zero_subtractionleft + S (pfs_left_division_zero_subtraction) = S ((S (pfs_index_division_zero_subtraction)) * ac)) /\ exists ff_q_pfp_division_zero_subtractionleft. ab = ff_q_pfp_division_zero_subtractionleft * S ((S (pfs_index_division_zero_subtraction)) * ac) + (pfs_left_division_zero_subtraction))) /\ (((((exists ff_h_pfp_division_zero_subtractionright. ff_h_pfp_division_zero_subtractionright + S (pfs_right_division_zero_subtraction) = S ((S (pfs_index_division_zero_subtraction)) * pc)) /\ exists ff_q_pfp_division_zero_subtractionright. pb = ff_q_pfp_division_zero_subtractionright * S ((S (pfs_index_division_zero_subtraction)) * pc) + (pfs_right_division_zero_subtraction))) /\ (((((exists ff_h_pfp_division_zero_subtractionresult. ff_h_pfp_division_zero_subtractionresult + S (pfs_result_division_zero_subtraction) = S ((S (pfs_index_division_zero_subtraction)) * uc)) /\ exists ff_q_pfp_division_zero_subtractionresult. ub = ff_q_pfp_division_zero_subtractionresult * S ((S (pfs_index_division_zero_subtraction)) * uc) + (pfs_result_division_zero_subtraction))) /\ ((((exists pfa_gap_division_zero_subtractionoperationleft. pfa_gap_division_zero_subtractionoperationleft + S (pfs_right_division_zero_subtraction) = (p)) /\ (((exists pfa_gap_division_zero_subtractionoperationright. pfa_gap_division_zero_subtractionoperationright + S (pfs_result_division_zero_subtraction) = (p)) /\ ((((exists pfa_gap_division_zero_subtractionoperationresultbound. pfa_gap_division_zero_subtractionoperationresultbound + S (pfs_left_division_zero_subtraction) = (p)) /\ ((exists pfa_offset_left_division_zero_subtractionoperationresultcongruence pfa_offset_right_division_zero_subtractionoperationresultcongruence. ((pfs_right_division_zero_subtraction) + (pfs_result_division_zero_subtraction)) + (p) * pfa_offset_left_division_zero_subtractionoperationresultcongruence = (pfs_left_division_zero_subtraction) + (p) * pfa_offset_right_division_zero_subtractionoperationresultcongruence)))))))))))))))) -> (forall pfp_repeat_index_division_zero_result. (exists pfa_gap_division_zero_resultindex. pfa_gap_division_zero_resultindex + S (pfp_repeat_index_division_zero_result) = (N)) -> (((exists ff_h_pfp_division_zero_resultentry. ff_h_pfp_division_zero_resultentry + S (0) = S ((S (pfp_repeat_index_division_zero_result)) * uc)) /\ exists ff_q_pfp_division_zero_resultentry. ub = ff_q_pfp_division_zero_resultentry * S ((S (pfp_repeat_index_division_zero_result)) * uc) + (0))))