prime_field_polynomial_quotient_prefix_product_matches

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc d qb qc N b pb pc L. (~((p) = 1) /\ forall pfa_factor_left_division_match_table_prime pfa_factor_right_division_match_table_prime. (p) = pfa_factor_left_division_match_table_prime * pfa_factor_right_division_match_table_prime -> pfa_factor_left_division_match_table_prime = 1 \/ pfa_factor_right_division_match_table_prime = 1) -> (((exists ff_h_pfp_division_match_table_head. ff_h_pfp_division_match_table_head + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_match_table_head. bb = ff_q_pfp_division_match_table_head * S ((S (0)) * bc) + (b))) -> (((~((b) = 0)) /\ ((((exists pfa_gap_division_match_table_inversemultiplicationleft. pfa_gap_division_match_table_inversemultiplicationleft + S (b) = (p)) /\ (((exists pfa_gap_division_match_table_inversemultiplicationright. pfa_gap_division_match_table_inversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_division_match_table_inversemultiplicationresultbound. pfa_gap_division_match_table_inversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_match_table_inversemultiplicationresultcongruence pfa_offset_right_division_match_table_inversemultiplicationresultcongruence. ((b) * (k)) + (p) * pfa_offset_left_division_match_table_inversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_match_table_inversemultiplicationresultcongruence)))))))))))) -> (forall pfd_index_division_match_table_execution. (exists pfa_gap_division_match_table_executionbound. pfa_gap_division_match_table_executionbound + S (pfd_index_division_match_table_execution) = (N)) -> exists pfd_value_division_match_table_execution. ((((exists ff_h_pfp_division_match_table_executionentry. ff_h_pfp_division_match_table_executionentry + S (pfd_value_division_match_table_execution) = S ((S (pfd_index_division_match_table_execution)) * qc)) /\ exists ff_q_pfp_division_match_table_executionentry. qb = ff_q_pfp_division_match_table_executionentry * S ((S (pfd_index_division_match_table_execution)) * qc) + (pfd_value_division_match_table_execution))) /\ ((exists pfd_input_division_match_table_executionstep pfd_previous_division_match_table_executionstep pfd_difference_division_match_table_executionstep. ((((exists ff_h_pfp_division_match_table_executionstepinput. ff_h_pfp_division_match_table_executionstepinput + S (pfd_input_division_match_table_executionstep) = S ((S (pfd_index_division_match_table_execution)) * ac)) /\ exists ff_q_pfp_division_match_table_executionstepinput. ab = ff_q_pfp_division_match_table_executionstepinput * S ((S (pfd_index_division_match_table_execution)) * ac) + (pfd_input_division_match_table_executionstep))) /\ (((exists pfc_terms_code_division_match_table_executionstepprevious pfc_terms_scale_division_match_table_executionstepprevious pfc_natural_sum_division_match_table_executionstepprevious. ((forall pfc_index_division_match_table_executionsteppreviousdiagonal. (exists pfa_gap_division_match_table_executionsteppreviousdiagonalbound. pfa_gap_division_match_table_executionsteppreviousdiagonalbound + S (pfc_index_division_match_table_executionsteppreviousdiagonal) = (S (pfd_index_division_match_table_execution))) -> exists pfc_value_division_match_table_executionsteppreviousdiagonal. ((((exists ff_h_pfp_division_match_table_executionsteppreviousdiagonalentry. ff_h_pfp_division_match_table_executionsteppreviousdiagonalentry + S (pfc_value_division_match_table_executionsteppreviousdiagonal) = S ((S (pfc_index_division_match_table_executionsteppreviousdiagonal)) * pfc_terms_scale_division_match_table_executionstepprevious)) /\ exists ff_q_pfp_division_match_table_executionsteppreviousdiagonalentry. pfc_terms_code_division_match_table_executionstepprevious = ff_q_pfp_division_match_table_executionsteppreviousdiagonalentry * S ((S (pfc_index_division_match_table_executionsteppreviousdiagonal)) * pfc_terms_scale_division_match_table_executionstepprevious) + (pfc_value_division_match_table_executionsteppreviousdiagonal))) /\ ((exists pfc_complement_division_match_table_executionsteppreviousdiagonalterm pfc_left_division_match_table_executionsteppreviousdiagonalterm pfc_right_division_match_table_executionsteppreviousdiagonalterm. (((pfc_index_division_match_table_executionsteppreviousdiagonal)+pfc_complement_division_match_table_executionsteppreviousdiagonalterm=(pfd_index_division_match_table_execution)) /\ ((((((exists pfa_gap_division_match_table_executionsteppreviousdiagonaltermleftinside. pfa_gap_division_match_table_executionsteppreviousdiagonaltermleftinside + S (pfc_index_division_match_table_executionsteppreviousdiagonal) = (pfd_index_division_match_table_execution)) /\ ((((exists ff_h_pfp_division_match_table_executionsteppreviousdiagonaltermleftentry. ff_h_pfp_division_match_table_executionsteppreviousdiagonaltermleftentry + S (pfc_left_division_match_table_executionsteppreviousdiagonalterm) = S ((S (pfc_index_division_match_table_executionsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_match_table_executionsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_match_table_executionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_match_table_executionsteppreviousdiagonal)) * qc) + (pfc_left_division_match_table_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_match_table_executionsteppreviousdiagonaltermleftoutside. pfc_gap_division_match_table_executionsteppreviousdiagonaltermleftoutside+(pfd_index_division_match_table_execution)=(pfc_index_division_match_table_executionsteppreviousdiagonal)) /\ (((pfc_left_division_match_table_executionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_match_table_executionsteppreviousdiagonaltermrightinside. pfa_gap_division_match_table_executionsteppreviousdiagonaltermrightinside + S (pfc_complement_division_match_table_executionsteppreviousdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_match_table_executionsteppreviousdiagonaltermrightentry. ff_h_pfp_division_match_table_executionsteppreviousdiagonaltermrightentry + S (pfc_right_division_match_table_executionsteppreviousdiagonalterm) = S ((S (pfc_complement_division_match_table_executionsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_match_table_executionsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_match_table_executionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_match_table_executionsteppreviousdiagonalterm)) * bc) + (pfc_right_division_match_table_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_match_table_executionsteppreviousdiagonaltermrightoutside. pfc_gap_division_match_table_executionsteppreviousdiagonaltermrightoutside+(S d)=(pfc_complement_division_match_table_executionsteppreviousdiagonalterm)) /\ (((pfc_right_division_match_table_executionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_match_table_executionsteppreviousdiagonal)=pfc_left_division_match_table_executionsteppreviousdiagonalterm*pfc_right_division_match_table_executionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_match_table_executionstepprevioussum fs_v_pfc_division_match_table_executionstepprevioussum. ((((exists fs_h_pfc_division_match_table_executionstepprevioussum_body_start. fs_h_pfc_division_match_table_executionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_match_table_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_table_executionstepprevioussum_body_start. fs_u_pfc_division_match_table_executionstepprevioussum = fs_q_pfc_division_match_table_executionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_match_table_executionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_match_table_executionstepprevioussum_body_terminal. fs_h_pfc_division_match_table_executionstepprevioussum_body_terminal + S (pfc_natural_sum_division_match_table_executionstepprevious) = S ((S (S (pfd_index_division_match_table_execution))) * fs_v_pfc_division_match_table_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_table_executionstepprevioussum_body_terminal. fs_u_pfc_division_match_table_executionstepprevioussum = fs_q_pfc_division_match_table_executionstepprevioussum_body_terminal * S ((S (S (pfd_index_division_match_table_execution))) * fs_v_pfc_division_match_table_executionstepprevioussum) + (pfc_natural_sum_division_match_table_executionstepprevious))) /\ forall fs_i_pfc_division_match_table_executionstepprevioussum_body_steps. (exists fs_lt_pfc_division_match_table_executionstepprevioussum_body_steps_bound. fs_lt_pfc_division_match_table_executionstepprevioussum_body_steps_bound + S fs_i_pfc_division_match_table_executionstepprevioussum_body_steps = S (pfd_index_division_match_table_execution)) -> exists fs_a_pfc_division_match_table_executionstepprevioussum_body_steps fs_r_pfc_division_match_table_executionstepprevioussum_body_steps fs_s_pfc_division_match_table_executionstepprevioussum_body_steps. ((((exists fs_h_pfc_division_match_table_executionstepprevioussum_body_steps_summand. fs_h_pfc_division_match_table_executionstepprevioussum_body_steps_summand + S (fs_a_pfc_division_match_table_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_match_table_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_match_table_executionstepprevious)) /\ exists fs_q_pfc_division_match_table_executionstepprevioussum_body_steps_summand. pfc_terms_code_division_match_table_executionstepprevious = fs_q_pfc_division_match_table_executionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_match_table_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_match_table_executionstepprevious) + (fs_a_pfc_division_match_table_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_match_table_executionstepprevioussum_body_steps_partial. fs_h_pfc_division_match_table_executionstepprevioussum_body_steps_partial + S (fs_r_pfc_division_match_table_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_match_table_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_table_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_table_executionstepprevioussum_body_steps_partial. fs_u_pfc_division_match_table_executionstepprevioussum = fs_q_pfc_division_match_table_executionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_match_table_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_table_executionstepprevioussum) + (fs_r_pfc_division_match_table_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_match_table_executionstepprevioussum_body_steps_successor. fs_h_pfc_division_match_table_executionstepprevioussum_body_steps_successor + S (fs_s_pfc_division_match_table_executionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_match_table_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_table_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_table_executionstepprevioussum_body_steps_successor. fs_u_pfc_division_match_table_executionstepprevioussum = fs_q_pfc_division_match_table_executionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_match_table_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_table_executionstepprevioussum) + (fs_s_pfc_division_match_table_executionstepprevioussum_body_steps))) /\ fs_s_pfc_division_match_table_executionstepprevioussum_body_steps = fs_r_pfc_division_match_table_executionstepprevioussum_body_steps + fs_a_pfc_division_match_table_executionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_match_table_executionsteppreviousresiduebound. pfa_gap_division_match_table_executionsteppreviousresiduebound + S (pfd_previous_division_match_table_executionstep) = (p)) /\ ((exists pfa_offset_left_division_match_table_executionsteppreviousresiduecongruence pfa_offset_right_division_match_table_executionsteppreviousresiduecongruence. (pfc_natural_sum_division_match_table_executionstepprevious) + (p) * pfa_offset_left_division_match_table_executionsteppreviousresiduecongruence = (pfd_previous_division_match_table_executionstep) + (p) * pfa_offset_right_division_match_table_executionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_match_table_executionstepsubtractleft. pfa_gap_division_match_table_executionstepsubtractleft + S (pfd_previous_division_match_table_executionstep) = (p)) /\ (((exists pfa_gap_division_match_table_executionstepsubtractright. pfa_gap_division_match_table_executionstepsubtractright + S (pfd_difference_division_match_table_executionstep) = (p)) /\ ((((exists pfa_gap_division_match_table_executionstepsubtractresultbound. pfa_gap_division_match_table_executionstepsubtractresultbound + S (pfd_input_division_match_table_executionstep) = (p)) /\ ((exists pfa_offset_left_division_match_table_executionstepsubtractresultcongruence pfa_offset_right_division_match_table_executionstepsubtractresultcongruence. ((pfd_previous_division_match_table_executionstep) + (pfd_difference_division_match_table_executionstep)) + (p) * pfa_offset_left_division_match_table_executionstepsubtractresultcongruence = (pfd_input_division_match_table_executionstep) + (p) * pfa_offset_right_division_match_table_executionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_match_table_executionstepmultiplyleft. pfa_gap_division_match_table_executionstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_match_table_executionstepmultiplyright. pfa_gap_division_match_table_executionstepmultiplyright + S (pfd_difference_division_match_table_executionstep) = (p)) /\ ((((exists pfa_gap_division_match_table_executionstepmultiplyresultbound. pfa_gap_division_match_table_executionstepmultiplyresultbound + S (pfd_value_division_match_table_execution) = (p)) /\ ((exists pfa_offset_left_division_match_table_executionstepmultiplyresultcongruence pfa_offset_right_division_match_table_executionstepmultiplyresultcongruence. ((k) * (pfd_difference_division_match_table_executionstep)) + (p) * pfa_offset_left_division_match_table_executionstepmultiplyresultcongruence = (pfd_value_division_match_table_execution) + (p) * pfa_offset_right_division_match_table_executionstepmultiplyresultcongruence))))))))))))))))))) -> (exists pfc_gap_division_match_table_length. pfc_gap_division_match_table_length+(N)=(L)) -> (forall pfc_index_division_match_table_product. (exists pfa_gap_division_match_table_productbound. pfa_gap_division_match_table_productbound + S (pfc_index_division_match_table_product) = (L)) -> exists pfc_value_division_match_table_product. ((((exists ff_h_pfp_division_match_table_productentry. ff_h_pfp_division_match_table_productentry + S (pfc_value_division_match_table_product) = S ((S (pfc_index_division_match_table_product)) * pc)) /\ exists ff_q_pfp_division_match_table_productentry. pb = ff_q_pfp_division_match_table_productentry * S ((S (pfc_index_division_match_table_product)) * pc) + (pfc_value_division_match_table_product))) /\ ((exists pfc_terms_code_division_match_table_productcoefficient pfc_terms_scale_division_match_table_productcoefficient pfc_natural_sum_division_match_table_productcoefficient. ((forall pfc_index_division_match_table_productcoefficientdiagonal. (exists pfa_gap_division_match_table_productcoefficientdiagonalbound. pfa_gap_division_match_table_productcoefficientdiagonalbound + S (pfc_index_division_match_table_productcoefficientdiagonal) = (S (pfc_index_division_match_table_product))) -> exists pfc_value_division_match_table_productcoefficientdiagonal. ((((exists ff_h_pfp_division_match_table_productcoefficientdiagonalentry. ff_h_pfp_division_match_table_productcoefficientdiagonalentry + S (pfc_value_division_match_table_productcoefficientdiagonal) = S ((S (pfc_index_division_match_table_productcoefficientdiagonal)) * pfc_terms_scale_division_match_table_productcoefficient)) /\ exists ff_q_pfp_division_match_table_productcoefficientdiagonalentry. pfc_terms_code_division_match_table_productcoefficient = ff_q_pfp_division_match_table_productcoefficientdiagonalentry * S ((S (pfc_index_division_match_table_productcoefficientdiagonal)) * pfc_terms_scale_division_match_table_productcoefficient) + (pfc_value_division_match_table_productcoefficientdiagonal))) /\ ((exists pfc_complement_division_match_table_productcoefficientdiagonalterm pfc_left_division_match_table_productcoefficientdiagonalterm pfc_right_division_match_table_productcoefficientdiagonalterm. (((pfc_index_division_match_table_productcoefficientdiagonal)+pfc_complement_division_match_table_productcoefficientdiagonalterm=(pfc_index_division_match_table_product)) /\ ((((((exists pfa_gap_division_match_table_productcoefficientdiagonaltermleftinside. pfa_gap_division_match_table_productcoefficientdiagonaltermleftinside + S (pfc_index_division_match_table_productcoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_division_match_table_productcoefficientdiagonaltermleftentry. ff_h_pfp_division_match_table_productcoefficientdiagonaltermleftentry + S (pfc_left_division_match_table_productcoefficientdiagonalterm) = S ((S (pfc_index_division_match_table_productcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_match_table_productcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_match_table_productcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_match_table_productcoefficientdiagonal)) * qc) + (pfc_left_division_match_table_productcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_match_table_productcoefficientdiagonaltermleftoutside. pfc_gap_division_match_table_productcoefficientdiagonaltermleftoutside+(N)=(pfc_index_division_match_table_productcoefficientdiagonal)) /\ (((pfc_left_division_match_table_productcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_match_table_productcoefficientdiagonaltermrightinside. pfa_gap_division_match_table_productcoefficientdiagonaltermrightinside + S (pfc_complement_division_match_table_productcoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_match_table_productcoefficientdiagonaltermrightentry. ff_h_pfp_division_match_table_productcoefficientdiagonaltermrightentry + S (pfc_right_division_match_table_productcoefficientdiagonalterm) = S ((S (pfc_complement_division_match_table_productcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_match_table_productcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_match_table_productcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_match_table_productcoefficientdiagonalterm)) * bc) + (pfc_right_division_match_table_productcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_match_table_productcoefficientdiagonaltermrightoutside. pfc_gap_division_match_table_productcoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_division_match_table_productcoefficientdiagonalterm)) /\ (((pfc_right_division_match_table_productcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_match_table_productcoefficientdiagonal)=pfc_left_division_match_table_productcoefficientdiagonalterm*pfc_right_division_match_table_productcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_match_table_productcoefficientsum fs_v_pfc_division_match_table_productcoefficientsum. ((((exists fs_h_pfc_division_match_table_productcoefficientsum_body_start. fs_h_pfc_division_match_table_productcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_match_table_productcoefficientsum)) /\ exists fs_q_pfc_division_match_table_productcoefficientsum_body_start. fs_u_pfc_division_match_table_productcoefficientsum = fs_q_pfc_division_match_table_productcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_match_table_productcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_match_table_productcoefficientsum_body_terminal. fs_h_pfc_division_match_table_productcoefficientsum_body_terminal + S (pfc_natural_sum_division_match_table_productcoefficient) = S ((S (S (pfc_index_division_match_table_product))) * fs_v_pfc_division_match_table_productcoefficientsum)) /\ exists fs_q_pfc_division_match_table_productcoefficientsum_body_terminal. fs_u_pfc_division_match_table_productcoefficientsum = fs_q_pfc_division_match_table_productcoefficientsum_body_terminal * S ((S (S (pfc_index_division_match_table_product))) * fs_v_pfc_division_match_table_productcoefficientsum) + (pfc_natural_sum_division_match_table_productcoefficient))) /\ forall fs_i_pfc_division_match_table_productcoefficientsum_body_steps. (exists fs_lt_pfc_division_match_table_productcoefficientsum_body_steps_bound. fs_lt_pfc_division_match_table_productcoefficientsum_body_steps_bound + S fs_i_pfc_division_match_table_productcoefficientsum_body_steps = S (pfc_index_division_match_table_product)) -> exists fs_a_pfc_division_match_table_productcoefficientsum_body_steps fs_r_pfc_division_match_table_productcoefficientsum_body_steps fs_s_pfc_division_match_table_productcoefficientsum_body_steps. ((((exists fs_h_pfc_division_match_table_productcoefficientsum_body_steps_summand. fs_h_pfc_division_match_table_productcoefficientsum_body_steps_summand + S (fs_a_pfc_division_match_table_productcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_match_table_productcoefficientsum_body_steps)) * pfc_terms_scale_division_match_table_productcoefficient)) /\ exists fs_q_pfc_division_match_table_productcoefficientsum_body_steps_summand. pfc_terms_code_division_match_table_productcoefficient = fs_q_pfc_division_match_table_productcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_match_table_productcoefficientsum_body_steps)) * pfc_terms_scale_division_match_table_productcoefficient) + (fs_a_pfc_division_match_table_productcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_match_table_productcoefficientsum_body_steps_partial. fs_h_pfc_division_match_table_productcoefficientsum_body_steps_partial + S (fs_r_pfc_division_match_table_productcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_match_table_productcoefficientsum_body_steps)) * fs_v_pfc_division_match_table_productcoefficientsum)) /\ exists fs_q_pfc_division_match_table_productcoefficientsum_body_steps_partial. fs_u_pfc_division_match_table_productcoefficientsum = fs_q_pfc_division_match_table_productcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_match_table_productcoefficientsum_body_steps)) * fs_v_pfc_division_match_table_productcoefficientsum) + (fs_r_pfc_division_match_table_productcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_match_table_productcoefficientsum_body_steps_successor. fs_h_pfc_division_match_table_productcoefficientsum_body_steps_successor + S (fs_s_pfc_division_match_table_productcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_match_table_productcoefficientsum_body_steps)) * fs_v_pfc_division_match_table_productcoefficientsum)) /\ exists fs_q_pfc_division_match_table_productcoefficientsum_body_steps_successor. fs_u_pfc_division_match_table_productcoefficientsum = fs_q_pfc_division_match_table_productcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_match_table_productcoefficientsum_body_steps)) * fs_v_pfc_division_match_table_productcoefficientsum) + (fs_s_pfc_division_match_table_productcoefficientsum_body_steps))) /\ fs_s_pfc_division_match_table_productcoefficientsum_body_steps = fs_r_pfc_division_match_table_productcoefficientsum_body_steps + fs_a_pfc_division_match_table_productcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_match_table_productcoefficientresiduebound. pfa_gap_division_match_table_productcoefficientresiduebound + S (pfc_value_division_match_table_product) = (p)) /\ ((exists pfa_offset_left_division_match_table_productcoefficientresiduecongruence pfa_offset_right_division_match_table_productcoefficientresiduecongruence. (pfc_natural_sum_division_match_table_productcoefficient) + (p) * pfa_offset_left_division_match_table_productcoefficientresiduecongruence = (pfc_value_division_match_table_product) + (p) * pfa_offset_right_division_match_table_productcoefficientresiduecongruence)))))))))))) -> (forall mdr_i_pfp_division_match_table_result mdr_a_pfp_division_match_table_result. (exists mdr_gap_pfp_division_match_table_resultb. mdr_gap_pfp_division_match_table_resultb + S (mdr_i_pfp_division_match_table_result) = (N)) -> (((exists ff_h_mdr_pfp_division_match_table_resulto. ff_h_mdr_pfp_division_match_table_resulto + S (mdr_a_pfp_division_match_table_result) = S ((S (mdr_i_pfp_division_match_table_result)) * ac)) /\ exists ff_q_mdr_pfp_division_match_table_resulto. ab = ff_q_mdr_pfp_division_match_table_resulto * S ((S (mdr_i_pfp_division_match_table_result)) * ac) + (mdr_a_pfp_division_match_table_result))) -> (((exists ff_h_mdr_pfp_division_match_table_resultn. ff_h_mdr_pfp_division_match_table_resultn + S (mdr_a_pfp_division_match_table_result) = S ((S (mdr_i_pfp_division_match_table_result)) * pc)) /\ exists ff_q_mdr_pfp_division_match_table_resultn. pb = ff_q_mdr_pfp_division_match_table_resultn * S ((S (mdr_i_pfp_division_match_table_result)) * pc) + (mdr_a_pfp_division_match_table_result))))