prime_field_polynomial_quotient_proper_product

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc d qb qc q pb pc L. (((((q)=0) /\ ((exists pfc_gap_division_product_chosen_lengthshort. pfc_gap_division_product_chosen_lengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) -> ~(q=0) -> (forall fom_index_pfp_division_product_divisor. (exists fom_gap_pfp_division_product_divisor_index_bound. fom_gap_pfp_division_product_divisor_index_bound + S (fom_index_pfp_division_product_divisor) = S d) -> exists fom_value_pfp_division_product_divisor. ((((exists fom_beta_height_pfp_division_product_divisor_entry. fom_beta_height_pfp_division_product_divisor_entry + S (fom_value_pfp_division_product_divisor) = S ((S (fom_index_pfp_division_product_divisor)) * bc)) /\ exists fom_beta_quotient_pfp_division_product_divisor_entry. bb = fom_beta_quotient_pfp_division_product_divisor_entry * S ((S (fom_index_pfp_division_product_divisor)) * bc) + (fom_value_pfp_division_product_divisor))) /\ (exists fom_gap_pfp_division_product_divisor_value_bound. fom_gap_pfp_division_product_divisor_value_bound + S (fom_value_pfp_division_product_divisor) = p))) -> (forall pfd_index_division_product_quotient. (exists pfa_gap_division_product_quotientbound. pfa_gap_division_product_quotientbound + S (pfd_index_division_product_quotient) = (q)) -> exists pfd_value_division_product_quotient. ((((exists ff_h_pfp_division_product_quotiententry. ff_h_pfp_division_product_quotiententry + S (pfd_value_division_product_quotient) = S ((S (pfd_index_division_product_quotient)) * qc)) /\ exists ff_q_pfp_division_product_quotiententry. qb = ff_q_pfp_division_product_quotiententry * S ((S (pfd_index_division_product_quotient)) * qc) + (pfd_value_division_product_quotient))) /\ ((exists pfd_input_division_product_quotientstep pfd_previous_division_product_quotientstep pfd_difference_division_product_quotientstep. ((((exists ff_h_pfp_division_product_quotientstepinput. ff_h_pfp_division_product_quotientstepinput + S (pfd_input_division_product_quotientstep) = S ((S (pfd_index_division_product_quotient)) * ac)) /\ exists ff_q_pfp_division_product_quotientstepinput. ab = ff_q_pfp_division_product_quotientstepinput * S ((S (pfd_index_division_product_quotient)) * ac) + (pfd_input_division_product_quotientstep))) /\ (((exists pfc_terms_code_division_product_quotientstepprevious pfc_terms_scale_division_product_quotientstepprevious pfc_natural_sum_division_product_quotientstepprevious. ((forall pfc_index_division_product_quotientsteppreviousdiagonal. (exists pfa_gap_division_product_quotientsteppreviousdiagonalbound. pfa_gap_division_product_quotientsteppreviousdiagonalbound + S (pfc_index_division_product_quotientsteppreviousdiagonal) = (S (pfd_index_division_product_quotient))) -> exists pfc_value_division_product_quotientsteppreviousdiagonal. ((((exists ff_h_pfp_division_product_quotientsteppreviousdiagonalentry. ff_h_pfp_division_product_quotientsteppreviousdiagonalentry + S (pfc_value_division_product_quotientsteppreviousdiagonal) = S ((S (pfc_index_division_product_quotientsteppreviousdiagonal)) * pfc_terms_scale_division_product_quotientstepprevious)) /\ exists ff_q_pfp_division_product_quotientsteppreviousdiagonalentry. pfc_terms_code_division_product_quotientstepprevious = ff_q_pfp_division_product_quotientsteppreviousdiagonalentry * S ((S (pfc_index_division_product_quotientsteppreviousdiagonal)) * pfc_terms_scale_division_product_quotientstepprevious) + (pfc_value_division_product_quotientsteppreviousdiagonal))) /\ ((exists pfc_complement_division_product_quotientsteppreviousdiagonalterm pfc_left_division_product_quotientsteppreviousdiagonalterm pfc_right_division_product_quotientsteppreviousdiagonalterm. (((pfc_index_division_product_quotientsteppreviousdiagonal)+pfc_complement_division_product_quotientsteppreviousdiagonalterm=(pfd_index_division_product_quotient)) /\ ((((((exists pfa_gap_division_product_quotientsteppreviousdiagonaltermleftinside. pfa_gap_division_product_quotientsteppreviousdiagonaltermleftinside + S (pfc_index_division_product_quotientsteppreviousdiagonal) = (pfd_index_division_product_quotient)) /\ ((((exists ff_h_pfp_division_product_quotientsteppreviousdiagonaltermleftentry. ff_h_pfp_division_product_quotientsteppreviousdiagonaltermleftentry + S (pfc_left_division_product_quotientsteppreviousdiagonalterm) = S ((S (pfc_index_division_product_quotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_product_quotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_product_quotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_product_quotientsteppreviousdiagonal)) * qc) + (pfc_left_division_product_quotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_product_quotientsteppreviousdiagonaltermleftoutside. pfc_gap_division_product_quotientsteppreviousdiagonaltermleftoutside+(pfd_index_division_product_quotient)=(pfc_index_division_product_quotientsteppreviousdiagonal)) /\ (((pfc_left_division_product_quotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_product_quotientsteppreviousdiagonaltermrightinside. pfa_gap_division_product_quotientsteppreviousdiagonaltermrightinside + S (pfc_complement_division_product_quotientsteppreviousdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_product_quotientsteppreviousdiagonaltermrightentry. ff_h_pfp_division_product_quotientsteppreviousdiagonaltermrightentry + S (pfc_right_division_product_quotientsteppreviousdiagonalterm) = S ((S (pfc_complement_division_product_quotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_product_quotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_product_quotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_product_quotientsteppreviousdiagonalterm)) * bc) + (pfc_right_division_product_quotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_product_quotientsteppreviousdiagonaltermrightoutside. pfc_gap_division_product_quotientsteppreviousdiagonaltermrightoutside+(S d)=(pfc_complement_division_product_quotientsteppreviousdiagonalterm)) /\ (((pfc_right_division_product_quotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_product_quotientsteppreviousdiagonal)=pfc_left_division_product_quotientsteppreviousdiagonalterm*pfc_right_division_product_quotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_product_quotientstepprevioussum fs_v_pfc_division_product_quotientstepprevioussum. ((((exists fs_h_pfc_division_product_quotientstepprevioussum_body_start. fs_h_pfc_division_product_quotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_product_quotientstepprevioussum)) /\ exists fs_q_pfc_division_product_quotientstepprevioussum_body_start. fs_u_pfc_division_product_quotientstepprevioussum = fs_q_pfc_division_product_quotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_product_quotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_product_quotientstepprevioussum_body_terminal. fs_h_pfc_division_product_quotientstepprevioussum_body_terminal + S (pfc_natural_sum_division_product_quotientstepprevious) = S ((S (S (pfd_index_division_product_quotient))) * fs_v_pfc_division_product_quotientstepprevioussum)) /\ exists fs_q_pfc_division_product_quotientstepprevioussum_body_terminal. fs_u_pfc_division_product_quotientstepprevioussum = fs_q_pfc_division_product_quotientstepprevioussum_body_terminal * S ((S (S (pfd_index_division_product_quotient))) * fs_v_pfc_division_product_quotientstepprevioussum) + (pfc_natural_sum_division_product_quotientstepprevious))) /\ forall fs_i_pfc_division_product_quotientstepprevioussum_body_steps. (exists fs_lt_pfc_division_product_quotientstepprevioussum_body_steps_bound. fs_lt_pfc_division_product_quotientstepprevioussum_body_steps_bound + S fs_i_pfc_division_product_quotientstepprevioussum_body_steps = S (pfd_index_division_product_quotient)) -> exists fs_a_pfc_division_product_quotientstepprevioussum_body_steps fs_r_pfc_division_product_quotientstepprevioussum_body_steps fs_s_pfc_division_product_quotientstepprevioussum_body_steps. ((((exists fs_h_pfc_division_product_quotientstepprevioussum_body_steps_summand. fs_h_pfc_division_product_quotientstepprevioussum_body_steps_summand + S (fs_a_pfc_division_product_quotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_product_quotientstepprevioussum_body_steps)) * pfc_terms_scale_division_product_quotientstepprevious)) /\ exists fs_q_pfc_division_product_quotientstepprevioussum_body_steps_summand. pfc_terms_code_division_product_quotientstepprevious = fs_q_pfc_division_product_quotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_product_quotientstepprevioussum_body_steps)) * pfc_terms_scale_division_product_quotientstepprevious) + (fs_a_pfc_division_product_quotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_product_quotientstepprevioussum_body_steps_partial. fs_h_pfc_division_product_quotientstepprevioussum_body_steps_partial + S (fs_r_pfc_division_product_quotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_product_quotientstepprevioussum_body_steps)) * fs_v_pfc_division_product_quotientstepprevioussum)) /\ exists fs_q_pfc_division_product_quotientstepprevioussum_body_steps_partial. fs_u_pfc_division_product_quotientstepprevioussum = fs_q_pfc_division_product_quotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_product_quotientstepprevioussum_body_steps)) * fs_v_pfc_division_product_quotientstepprevioussum) + (fs_r_pfc_division_product_quotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_product_quotientstepprevioussum_body_steps_successor. fs_h_pfc_division_product_quotientstepprevioussum_body_steps_successor + S (fs_s_pfc_division_product_quotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_product_quotientstepprevioussum_body_steps)) * fs_v_pfc_division_product_quotientstepprevioussum)) /\ exists fs_q_pfc_division_product_quotientstepprevioussum_body_steps_successor. fs_u_pfc_division_product_quotientstepprevioussum = fs_q_pfc_division_product_quotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_product_quotientstepprevioussum_body_steps)) * fs_v_pfc_division_product_quotientstepprevioussum) + (fs_s_pfc_division_product_quotientstepprevioussum_body_steps))) /\ fs_s_pfc_division_product_quotientstepprevioussum_body_steps = fs_r_pfc_division_product_quotientstepprevioussum_body_steps + fs_a_pfc_division_product_quotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_product_quotientsteppreviousresiduebound. pfa_gap_division_product_quotientsteppreviousresiduebound + S (pfd_previous_division_product_quotientstep) = (p)) /\ ((exists pfa_offset_left_division_product_quotientsteppreviousresiduecongruence pfa_offset_right_division_product_quotientsteppreviousresiduecongruence. (pfc_natural_sum_division_product_quotientstepprevious) + (p) * pfa_offset_left_division_product_quotientsteppreviousresiduecongruence = (pfd_previous_division_product_quotientstep) + (p) * pfa_offset_right_division_product_quotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_product_quotientstepsubtractleft. pfa_gap_division_product_quotientstepsubtractleft + S (pfd_previous_division_product_quotientstep) = (p)) /\ (((exists pfa_gap_division_product_quotientstepsubtractright. pfa_gap_division_product_quotientstepsubtractright + S (pfd_difference_division_product_quotientstep) = (p)) /\ ((((exists pfa_gap_division_product_quotientstepsubtractresultbound. pfa_gap_division_product_quotientstepsubtractresultbound + S (pfd_input_division_product_quotientstep) = (p)) /\ ((exists pfa_offset_left_division_product_quotientstepsubtractresultcongruence pfa_offset_right_division_product_quotientstepsubtractresultcongruence. ((pfd_previous_division_product_quotientstep) + (pfd_difference_division_product_quotientstep)) + (p) * pfa_offset_left_division_product_quotientstepsubtractresultcongruence = (pfd_input_division_product_quotientstep) + (p) * pfa_offset_right_division_product_quotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_product_quotientstepmultiplyleft. pfa_gap_division_product_quotientstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_product_quotientstepmultiplyright. pfa_gap_division_product_quotientstepmultiplyright + S (pfd_difference_division_product_quotientstep) = (p)) /\ ((((exists pfa_gap_division_product_quotientstepmultiplyresultbound. pfa_gap_division_product_quotientstepmultiplyresultbound + S (pfd_value_division_product_quotient) = (p)) /\ ((exists pfa_offset_left_division_product_quotientstepmultiplyresultcongruence pfa_offset_right_division_product_quotientstepmultiplyresultcongruence. ((k) * (pfd_difference_division_product_quotientstep)) + (p) * pfa_offset_left_division_product_quotientstepmultiplyresultcongruence = (pfd_value_division_product_quotient) + (p) * pfa_offset_right_division_product_quotientstepmultiplyresultcongruence))))))))))))))))))) -> (forall pfc_index_division_product_ambient. (exists pfa_gap_division_product_ambientbound. pfa_gap_division_product_ambientbound + S (pfc_index_division_product_ambient) = (L)) -> exists pfc_value_division_product_ambient. ((((exists ff_h_pfp_division_product_ambiententry. ff_h_pfp_division_product_ambiententry + S (pfc_value_division_product_ambient) = S ((S (pfc_index_division_product_ambient)) * pc)) /\ exists ff_q_pfp_division_product_ambiententry. pb = ff_q_pfp_division_product_ambiententry * S ((S (pfc_index_division_product_ambient)) * pc) + (pfc_value_division_product_ambient))) /\ ((exists pfc_terms_code_division_product_ambientcoefficient pfc_terms_scale_division_product_ambientcoefficient pfc_natural_sum_division_product_ambientcoefficient. ((forall pfc_index_division_product_ambientcoefficientdiagonal. (exists pfa_gap_division_product_ambientcoefficientdiagonalbound. pfa_gap_division_product_ambientcoefficientdiagonalbound + S (pfc_index_division_product_ambientcoefficientdiagonal) = (S (pfc_index_division_product_ambient))) -> exists pfc_value_division_product_ambientcoefficientdiagonal. ((((exists ff_h_pfp_division_product_ambientcoefficientdiagonalentry. ff_h_pfp_division_product_ambientcoefficientdiagonalentry + S (pfc_value_division_product_ambientcoefficientdiagonal) = S ((S (pfc_index_division_product_ambientcoefficientdiagonal)) * pfc_terms_scale_division_product_ambientcoefficient)) /\ exists ff_q_pfp_division_product_ambientcoefficientdiagonalentry. pfc_terms_code_division_product_ambientcoefficient = ff_q_pfp_division_product_ambientcoefficientdiagonalentry * S ((S (pfc_index_division_product_ambientcoefficientdiagonal)) * pfc_terms_scale_division_product_ambientcoefficient) + (pfc_value_division_product_ambientcoefficientdiagonal))) /\ ((exists pfc_complement_division_product_ambientcoefficientdiagonalterm pfc_left_division_product_ambientcoefficientdiagonalterm pfc_right_division_product_ambientcoefficientdiagonalterm. (((pfc_index_division_product_ambientcoefficientdiagonal)+pfc_complement_division_product_ambientcoefficientdiagonalterm=(pfc_index_division_product_ambient)) /\ ((((((exists pfa_gap_division_product_ambientcoefficientdiagonaltermleftinside. pfa_gap_division_product_ambientcoefficientdiagonaltermleftinside + S (pfc_index_division_product_ambientcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_product_ambientcoefficientdiagonaltermleftentry. ff_h_pfp_division_product_ambientcoefficientdiagonaltermleftentry + S (pfc_left_division_product_ambientcoefficientdiagonalterm) = S ((S (pfc_index_division_product_ambientcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_product_ambientcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_product_ambientcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_product_ambientcoefficientdiagonal)) * qc) + (pfc_left_division_product_ambientcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_product_ambientcoefficientdiagonaltermleftoutside. pfc_gap_division_product_ambientcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_product_ambientcoefficientdiagonal)) /\ (((pfc_left_division_product_ambientcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_product_ambientcoefficientdiagonaltermrightinside. pfa_gap_division_product_ambientcoefficientdiagonaltermrightinside + S (pfc_complement_division_product_ambientcoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_product_ambientcoefficientdiagonaltermrightentry. ff_h_pfp_division_product_ambientcoefficientdiagonaltermrightentry + S (pfc_right_division_product_ambientcoefficientdiagonalterm) = S ((S (pfc_complement_division_product_ambientcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_product_ambientcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_product_ambientcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_product_ambientcoefficientdiagonalterm)) * bc) + (pfc_right_division_product_ambientcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_product_ambientcoefficientdiagonaltermrightoutside. pfc_gap_division_product_ambientcoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_division_product_ambientcoefficientdiagonalterm)) /\ (((pfc_right_division_product_ambientcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_product_ambientcoefficientdiagonal)=pfc_left_division_product_ambientcoefficientdiagonalterm*pfc_right_division_product_ambientcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_product_ambientcoefficientsum fs_v_pfc_division_product_ambientcoefficientsum. ((((exists fs_h_pfc_division_product_ambientcoefficientsum_body_start. fs_h_pfc_division_product_ambientcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_product_ambientcoefficientsum)) /\ exists fs_q_pfc_division_product_ambientcoefficientsum_body_start. fs_u_pfc_division_product_ambientcoefficientsum = fs_q_pfc_division_product_ambientcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_product_ambientcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_product_ambientcoefficientsum_body_terminal. fs_h_pfc_division_product_ambientcoefficientsum_body_terminal + S (pfc_natural_sum_division_product_ambientcoefficient) = S ((S (S (pfc_index_division_product_ambient))) * fs_v_pfc_division_product_ambientcoefficientsum)) /\ exists fs_q_pfc_division_product_ambientcoefficientsum_body_terminal. fs_u_pfc_division_product_ambientcoefficientsum = fs_q_pfc_division_product_ambientcoefficientsum_body_terminal * S ((S (S (pfc_index_division_product_ambient))) * fs_v_pfc_division_product_ambientcoefficientsum) + (pfc_natural_sum_division_product_ambientcoefficient))) /\ forall fs_i_pfc_division_product_ambientcoefficientsum_body_steps. (exists fs_lt_pfc_division_product_ambientcoefficientsum_body_steps_bound. fs_lt_pfc_division_product_ambientcoefficientsum_body_steps_bound + S fs_i_pfc_division_product_ambientcoefficientsum_body_steps = S (pfc_index_division_product_ambient)) -> exists fs_a_pfc_division_product_ambientcoefficientsum_body_steps fs_r_pfc_division_product_ambientcoefficientsum_body_steps fs_s_pfc_division_product_ambientcoefficientsum_body_steps. ((((exists fs_h_pfc_division_product_ambientcoefficientsum_body_steps_summand. fs_h_pfc_division_product_ambientcoefficientsum_body_steps_summand + S (fs_a_pfc_division_product_ambientcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_product_ambientcoefficientsum_body_steps)) * pfc_terms_scale_division_product_ambientcoefficient)) /\ exists fs_q_pfc_division_product_ambientcoefficientsum_body_steps_summand. pfc_terms_code_division_product_ambientcoefficient = fs_q_pfc_division_product_ambientcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_product_ambientcoefficientsum_body_steps)) * pfc_terms_scale_division_product_ambientcoefficient) + (fs_a_pfc_division_product_ambientcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_product_ambientcoefficientsum_body_steps_partial. fs_h_pfc_division_product_ambientcoefficientsum_body_steps_partial + S (fs_r_pfc_division_product_ambientcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_product_ambientcoefficientsum_body_steps)) * fs_v_pfc_division_product_ambientcoefficientsum)) /\ exists fs_q_pfc_division_product_ambientcoefficientsum_body_steps_partial. fs_u_pfc_division_product_ambientcoefficientsum = fs_q_pfc_division_product_ambientcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_product_ambientcoefficientsum_body_steps)) * fs_v_pfc_division_product_ambientcoefficientsum) + (fs_r_pfc_division_product_ambientcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_product_ambientcoefficientsum_body_steps_successor. fs_h_pfc_division_product_ambientcoefficientsum_body_steps_successor + S (fs_s_pfc_division_product_ambientcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_product_ambientcoefficientsum_body_steps)) * fs_v_pfc_division_product_ambientcoefficientsum)) /\ exists fs_q_pfc_division_product_ambientcoefficientsum_body_steps_successor. fs_u_pfc_division_product_ambientcoefficientsum = fs_q_pfc_division_product_ambientcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_product_ambientcoefficientsum_body_steps)) * fs_v_pfc_division_product_ambientcoefficientsum) + (fs_s_pfc_division_product_ambientcoefficientsum_body_steps))) /\ fs_s_pfc_division_product_ambientcoefficientsum_body_steps = fs_r_pfc_division_product_ambientcoefficientsum_body_steps + fs_a_pfc_division_product_ambientcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_product_ambientcoefficientresiduebound. pfa_gap_division_product_ambientcoefficientresiduebound + S (pfc_value_division_product_ambient) = (p)) /\ ((exists pfa_offset_left_division_product_ambientcoefficientresiduecongruence pfa_offset_right_division_product_ambientcoefficientresiduecongruence. (pfc_natural_sum_division_product_ambientcoefficient) + (p) * pfa_offset_left_division_product_ambientcoefficientresiduecongruence = (pfc_value_division_product_ambient) + (p) * pfa_offset_right_division_product_ambientcoefficientresiduecongruence)))))))))))) -> (((forall fom_index_pfp_division_product_actualleft. (exists fom_gap_pfp_division_product_actualleft_index_bound. fom_gap_pfp_division_product_actualleft_index_bound + S (fom_index_pfp_division_product_actualleft) = q) -> exists fom_value_pfp_division_product_actualleft. ((((exists fom_beta_height_pfp_division_product_actualleft_entry. fom_beta_height_pfp_division_product_actualleft_entry + S (fom_value_pfp_division_product_actualleft) = S ((S (fom_index_pfp_division_product_actualleft)) * qc)) /\ exists fom_beta_quotient_pfp_division_product_actualleft_entry. qb = fom_beta_quotient_pfp_division_product_actualleft_entry * S ((S (fom_index_pfp_division_product_actualleft)) * qc) + (fom_value_pfp_division_product_actualleft))) /\ (exists fom_gap_pfp_division_product_actualleft_value_bound. fom_gap_pfp_division_product_actualleft_value_bound + S (fom_value_pfp_division_product_actualleft) = p))) /\ (((forall fom_index_pfp_division_product_actualright. (exists fom_gap_pfp_division_product_actualright_index_bound. fom_gap_pfp_division_product_actualright_index_bound + S (fom_index_pfp_division_product_actualright) = S d) -> exists fom_value_pfp_division_product_actualright. ((((exists fom_beta_height_pfp_division_product_actualright_entry. fom_beta_height_pfp_division_product_actualright_entry + S (fom_value_pfp_division_product_actualright) = S ((S (fom_index_pfp_division_product_actualright)) * bc)) /\ exists fom_beta_quotient_pfp_division_product_actualright_entry. bb = fom_beta_quotient_pfp_division_product_actualright_entry * S ((S (fom_index_pfp_division_product_actualright)) * bc) + (fom_value_pfp_division_product_actualright))) /\ (exists fom_gap_pfp_division_product_actualright_value_bound. fom_gap_pfp_division_product_actualright_value_bound + S (fom_value_pfp_division_product_actualright) = p))) /\ (((((((q)=0 \/ (S d)=0) /\ (((L)=0)))) \/ (((~((q)=0)) /\ (((~((S d)=0)) /\ (((q)+(S d)=S (L)))))))) /\ ((forall pfc_index_division_product_actualcoefficients. (exists pfa_gap_division_product_actualcoefficientsbound. pfa_gap_division_product_actualcoefficientsbound + S (pfc_index_division_product_actualcoefficients) = (L)) -> exists pfc_value_division_product_actualcoefficients. ((((exists ff_h_pfp_division_product_actualcoefficientsentry. ff_h_pfp_division_product_actualcoefficientsentry + S (pfc_value_division_product_actualcoefficients) = S ((S (pfc_index_division_product_actualcoefficients)) * pc)) /\ exists ff_q_pfp_division_product_actualcoefficientsentry. pb = ff_q_pfp_division_product_actualcoefficientsentry * S ((S (pfc_index_division_product_actualcoefficients)) * pc) + (pfc_value_division_product_actualcoefficients))) /\ ((exists pfc_terms_code_division_product_actualcoefficientscoefficient pfc_terms_scale_division_product_actualcoefficientscoefficient pfc_natural_sum_division_product_actualcoefficientscoefficient. ((forall pfc_index_division_product_actualcoefficientscoefficientdiagonal. (exists pfa_gap_division_product_actualcoefficientscoefficientdiagonalbound. pfa_gap_division_product_actualcoefficientscoefficientdiagonalbound + S (pfc_index_division_product_actualcoefficientscoefficientdiagonal) = (S (pfc_index_division_product_actualcoefficients))) -> exists pfc_value_division_product_actualcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_division_product_actualcoefficientscoefficientdiagonalentry. ff_h_pfp_division_product_actualcoefficientscoefficientdiagonalentry + S (pfc_value_division_product_actualcoefficientscoefficientdiagonal) = S ((S (pfc_index_division_product_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_division_product_actualcoefficientscoefficient)) /\ exists ff_q_pfp_division_product_actualcoefficientscoefficientdiagonalentry. pfc_terms_code_division_product_actualcoefficientscoefficient = ff_q_pfp_division_product_actualcoefficientscoefficientdiagonalentry * S ((S (pfc_index_division_product_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_division_product_actualcoefficientscoefficient) + (pfc_value_division_product_actualcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_division_product_actualcoefficientscoefficientdiagonalterm pfc_left_division_product_actualcoefficientscoefficientdiagonalterm pfc_right_division_product_actualcoefficientscoefficientdiagonalterm. (((pfc_index_division_product_actualcoefficientscoefficientdiagonal)+pfc_complement_division_product_actualcoefficientscoefficientdiagonalterm=(pfc_index_division_product_actualcoefficients)) /\ ((((((exists pfa_gap_division_product_actualcoefficientscoefficientdiagonaltermleftinside. pfa_gap_division_product_actualcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_division_product_actualcoefficientscoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_product_actualcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_division_product_actualcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_division_product_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_division_product_actualcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_product_actualcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_product_actualcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_division_product_actualcoefficientscoefficientdiagonal)) * qc) + (pfc_left_division_product_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_product_actualcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_division_product_actualcoefficientscoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_product_actualcoefficientscoefficientdiagonal)) /\ (((pfc_left_division_product_actualcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_product_actualcoefficientscoefficientdiagonaltermrightinside. pfa_gap_division_product_actualcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_division_product_actualcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_product_actualcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_division_product_actualcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_division_product_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_division_product_actualcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_product_actualcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_product_actualcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_product_actualcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_division_product_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_product_actualcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_division_product_actualcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_division_product_actualcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_division_product_actualcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_product_actualcoefficientscoefficientdiagonal)=pfc_left_division_product_actualcoefficientscoefficientdiagonalterm*pfc_right_division_product_actualcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_product_actualcoefficientscoefficientsum fs_v_pfc_division_product_actualcoefficientscoefficientsum. ((((exists fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_start. fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_start. fs_u_pfc_division_product_actualcoefficientscoefficientsum = fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_product_actualcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_terminal. fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_division_product_actualcoefficientscoefficient) = S ((S (S (pfc_index_division_product_actualcoefficients))) * fs_v_pfc_division_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_terminal. fs_u_pfc_division_product_actualcoefficientscoefficientsum = fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_division_product_actualcoefficients))) * fs_v_pfc_division_product_actualcoefficientscoefficientsum) + (pfc_natural_sum_division_product_actualcoefficientscoefficient))) /\ forall fs_i_pfc_division_product_actualcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_division_product_actualcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_division_product_actualcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_division_product_actualcoefficientscoefficientsum_body_steps = S (pfc_index_division_product_actualcoefficients)) -> exists fs_a_pfc_division_product_actualcoefficientscoefficientsum_body_steps fs_r_pfc_division_product_actualcoefficientscoefficientsum_body_steps fs_s_pfc_division_product_actualcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_division_product_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_division_product_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_division_product_actualcoefficientscoefficient)) /\ exists fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_division_product_actualcoefficientscoefficient = fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_product_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_division_product_actualcoefficientscoefficient) + (fs_a_pfc_division_product_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_division_product_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_division_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_division_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_division_product_actualcoefficientscoefficientsum = fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_division_product_actualcoefficientscoefficientsum) + (fs_r_pfc_division_product_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_division_product_actualcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_division_product_actualcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_division_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_division_product_actualcoefficientscoefficientsum = fs_q_pfc_division_product_actualcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_division_product_actualcoefficientscoefficientsum) + (fs_s_pfc_division_product_actualcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_division_product_actualcoefficientscoefficientsum_body_steps = fs_r_pfc_division_product_actualcoefficientscoefficientsum_body_steps + fs_a_pfc_division_product_actualcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_product_actualcoefficientscoefficientresiduebound. pfa_gap_division_product_actualcoefficientscoefficientresiduebound + S (pfc_value_division_product_actualcoefficients) = (p)) /\ ((exists pfa_offset_left_division_product_actualcoefficientscoefficientresiduecongruence pfa_offset_right_division_product_actualcoefficientscoefficientresiduecongruence. (pfc_natural_sum_division_product_actualcoefficientscoefficient) + (p) * pfa_offset_left_division_product_actualcoefficientscoefficientresiduecongruence = (pfc_value_division_product_actualcoefficients) + (p) * pfa_offset_right_division_product_actualcoefficientscoefficientresiduecongruence)))))))))))))))))))