prime_field_polynomial_division_remainder_degree

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc d qb qc q rb rc R. (~((p) = 1) /\ forall pfa_factor_left_division_degree_prime pfa_factor_right_division_degree_prime. (p) = pfa_factor_left_division_degree_prime * pfa_factor_right_division_degree_prime -> pfa_factor_left_division_degree_prime = 1 \/ pfa_factor_right_division_degree_prime = 1) -> (((forall fom_index_pfp_division_degree_executioninput. (exists fom_gap_pfp_division_degree_executioninput_index_bound. fom_gap_pfp_division_degree_executioninput_index_bound + S (fom_index_pfp_division_degree_executioninput) = L) -> exists fom_value_pfp_division_degree_executioninput. ((((exists fom_beta_height_pfp_division_degree_executioninput_entry. fom_beta_height_pfp_division_degree_executioninput_entry + S (fom_value_pfp_division_degree_executioninput) = S ((S (fom_index_pfp_division_degree_executioninput)) * ac)) /\ exists fom_beta_quotient_pfp_division_degree_executioninput_entry. ab = fom_beta_quotient_pfp_division_degree_executioninput_entry * S ((S (fom_index_pfp_division_degree_executioninput)) * ac) + (fom_value_pfp_division_degree_executioninput))) /\ (exists fom_gap_pfp_division_degree_executioninput_value_bound. fom_gap_pfp_division_degree_executioninput_value_bound + S (fom_value_pfp_division_degree_executioninput) = p))) /\ (((forall fom_index_pfp_division_degree_executiondivisor. (exists fom_gap_pfp_division_degree_executiondivisor_index_bound. fom_gap_pfp_division_degree_executiondivisor_index_bound + S (fom_index_pfp_division_degree_executiondivisor) = S (d)) -> exists fom_value_pfp_division_degree_executiondivisor. ((((exists fom_beta_height_pfp_division_degree_executiondivisor_entry. fom_beta_height_pfp_division_degree_executiondivisor_entry + S (fom_value_pfp_division_degree_executiondivisor) = S ((S (fom_index_pfp_division_degree_executiondivisor)) * bc)) /\ exists fom_beta_quotient_pfp_division_degree_executiondivisor_entry. bb = fom_beta_quotient_pfp_division_degree_executiondivisor_entry * S ((S (fom_index_pfp_division_degree_executiondivisor)) * bc) + (fom_value_pfp_division_degree_executiondivisor))) /\ (exists fom_gap_pfp_division_degree_executiondivisor_value_bound. fom_gap_pfp_division_degree_executiondivisor_value_bound + S (fom_value_pfp_division_degree_executiondivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_division_degree_executionlengthshort. pfc_gap_division_degree_executionlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_division_degree_execution pfd_inverse_division_degree_execution pfd_product_code_division_degree_execution pfd_product_scale_division_degree_execution pfd_residual_code_division_degree_execution pfd_residual_scale_division_degree_execution pfd_cut_division_degree_execution. ((((exists ff_h_pfp_division_degree_executionhead. ff_h_pfp_division_degree_executionhead + S (pfd_head_division_degree_execution) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_degree_executionhead. bb = ff_q_pfp_division_degree_executionhead * S ((S (0)) * bc) + (pfd_head_division_degree_execution))) /\ (((((~((pfd_head_division_degree_execution) = 0)) /\ ((((exists pfa_gap_division_degree_executioninversemultiplicationleft. pfa_gap_division_degree_executioninversemultiplicationleft + S (pfd_head_division_degree_execution) = (p)) /\ (((exists pfa_gap_division_degree_executioninversemultiplicationright. pfa_gap_division_degree_executioninversemultiplicationright + S (pfd_inverse_division_degree_execution) = (p)) /\ ((((exists pfa_gap_division_degree_executioninversemultiplicationresultbound. pfa_gap_division_degree_executioninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_degree_executioninversemultiplicationresultcongruence pfa_offset_right_division_degree_executioninversemultiplicationresultcongruence. ((pfd_head_division_degree_execution) * (pfd_inverse_division_degree_execution)) + (p) * pfa_offset_left_division_degree_executioninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_degree_executioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_division_degree_executionquotient. (exists pfa_gap_division_degree_executionquotientbound. pfa_gap_division_degree_executionquotientbound + S (pfd_index_division_degree_executionquotient) = (q)) -> exists pfd_value_division_degree_executionquotient. ((((exists ff_h_pfp_division_degree_executionquotiententry. ff_h_pfp_division_degree_executionquotiententry + S (pfd_value_division_degree_executionquotient) = S ((S (pfd_index_division_degree_executionquotient)) * qc)) /\ exists ff_q_pfp_division_degree_executionquotiententry. qb = ff_q_pfp_division_degree_executionquotiententry * S ((S (pfd_index_division_degree_executionquotient)) * qc) + (pfd_value_division_degree_executionquotient))) /\ ((exists pfd_input_division_degree_executionquotientstep pfd_previous_division_degree_executionquotientstep pfd_difference_division_degree_executionquotientstep. ((((exists ff_h_pfp_division_degree_executionquotientstepinput. ff_h_pfp_division_degree_executionquotientstepinput + S (pfd_input_division_degree_executionquotientstep) = S ((S (pfd_index_division_degree_executionquotient)) * ac)) /\ exists ff_q_pfp_division_degree_executionquotientstepinput. ab = ff_q_pfp_division_degree_executionquotientstepinput * S ((S (pfd_index_division_degree_executionquotient)) * ac) + (pfd_input_division_degree_executionquotientstep))) /\ (((exists pfc_terms_code_division_degree_executionquotientstepprevious pfc_terms_scale_division_degree_executionquotientstepprevious pfc_natural_sum_division_degree_executionquotientstepprevious. ((forall pfc_index_division_degree_executionquotientsteppreviousdiagonal. (exists pfa_gap_division_degree_executionquotientsteppreviousdiagonalbound. pfa_gap_division_degree_executionquotientsteppreviousdiagonalbound + S (pfc_index_division_degree_executionquotientsteppreviousdiagonal) = (S (pfd_index_division_degree_executionquotient))) -> exists pfc_value_division_degree_executionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_division_degree_executionquotientsteppreviousdiagonalentry. ff_h_pfp_division_degree_executionquotientsteppreviousdiagonalentry + S (pfc_value_division_degree_executionquotientsteppreviousdiagonal) = S ((S (pfc_index_division_degree_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_division_degree_executionquotientstepprevious)) /\ exists ff_q_pfp_division_degree_executionquotientsteppreviousdiagonalentry. pfc_terms_code_division_degree_executionquotientstepprevious = ff_q_pfp_division_degree_executionquotientsteppreviousdiagonalentry * S ((S (pfc_index_division_degree_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_division_degree_executionquotientstepprevious) + (pfc_value_division_degree_executionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_division_degree_executionquotientsteppreviousdiagonalterm pfc_left_division_degree_executionquotientsteppreviousdiagonalterm pfc_right_division_degree_executionquotientsteppreviousdiagonalterm. (((pfc_index_division_degree_executionquotientsteppreviousdiagonal)+pfc_complement_division_degree_executionquotientsteppreviousdiagonalterm=(pfd_index_division_degree_executionquotient)) /\ ((((((exists pfa_gap_division_degree_executionquotientsteppreviousdiagonaltermleftinside. pfa_gap_division_degree_executionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_division_degree_executionquotientsteppreviousdiagonal) = (pfd_index_division_degree_executionquotient)) /\ ((((exists ff_h_pfp_division_degree_executionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_division_degree_executionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_division_degree_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_division_degree_executionquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_degree_executionquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_degree_executionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_degree_executionquotientsteppreviousdiagonal)) * qc) + (pfc_left_division_degree_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_degree_executionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_division_degree_executionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_division_degree_executionquotient)=(pfc_index_division_degree_executionquotientsteppreviousdiagonal)) /\ (((pfc_left_division_degree_executionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_degree_executionquotientsteppreviousdiagonaltermrightinside. pfa_gap_division_degree_executionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_division_degree_executionquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_degree_executionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_division_degree_executionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_division_degree_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_division_degree_executionquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_degree_executionquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_degree_executionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_degree_executionquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_division_degree_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_degree_executionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_division_degree_executionquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_division_degree_executionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_division_degree_executionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_degree_executionquotientsteppreviousdiagonal)=pfc_left_division_degree_executionquotientsteppreviousdiagonalterm*pfc_right_division_degree_executionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_degree_executionquotientstepprevioussum fs_v_pfc_division_degree_executionquotientstepprevioussum. ((((exists fs_h_pfc_division_degree_executionquotientstepprevioussum_body_start. fs_h_pfc_division_degree_executionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_degree_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_degree_executionquotientstepprevioussum_body_start. fs_u_pfc_division_degree_executionquotientstepprevioussum = fs_q_pfc_division_degree_executionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_degree_executionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_degree_executionquotientstepprevioussum_body_terminal. fs_h_pfc_division_degree_executionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_division_degree_executionquotientstepprevious) = S ((S (S (pfd_index_division_degree_executionquotient))) * fs_v_pfc_division_degree_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_degree_executionquotientstepprevioussum_body_terminal. fs_u_pfc_division_degree_executionquotientstepprevioussum = fs_q_pfc_division_degree_executionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_division_degree_executionquotient))) * fs_v_pfc_division_degree_executionquotientstepprevioussum) + (pfc_natural_sum_division_degree_executionquotientstepprevious))) /\ forall fs_i_pfc_division_degree_executionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_division_degree_executionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_division_degree_executionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_division_degree_executionquotientstepprevioussum_body_steps = S (pfd_index_division_degree_executionquotient)) -> exists fs_a_pfc_division_degree_executionquotientstepprevioussum_body_steps fs_r_pfc_division_degree_executionquotientstepprevioussum_body_steps fs_s_pfc_division_degree_executionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_division_degree_executionquotientstepprevioussum_body_steps_summand. fs_h_pfc_division_degree_executionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_division_degree_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_degree_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_degree_executionquotientstepprevious)) /\ exists fs_q_pfc_division_degree_executionquotientstepprevioussum_body_steps_summand. pfc_terms_code_division_degree_executionquotientstepprevious = fs_q_pfc_division_degree_executionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_degree_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_degree_executionquotientstepprevious) + (fs_a_pfc_division_degree_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_degree_executionquotientstepprevioussum_body_steps_partial. fs_h_pfc_division_degree_executionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_division_degree_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_degree_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_degree_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_degree_executionquotientstepprevioussum_body_steps_partial. fs_u_pfc_division_degree_executionquotientstepprevioussum = fs_q_pfc_division_degree_executionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_degree_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_degree_executionquotientstepprevioussum) + (fs_r_pfc_division_degree_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_degree_executionquotientstepprevioussum_body_steps_successor. fs_h_pfc_division_degree_executionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_division_degree_executionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_degree_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_degree_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_degree_executionquotientstepprevioussum_body_steps_successor. fs_u_pfc_division_degree_executionquotientstepprevioussum = fs_q_pfc_division_degree_executionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_degree_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_degree_executionquotientstepprevioussum) + (fs_s_pfc_division_degree_executionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_division_degree_executionquotientstepprevioussum_body_steps = fs_r_pfc_division_degree_executionquotientstepprevioussum_body_steps + fs_a_pfc_division_degree_executionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_degree_executionquotientsteppreviousresiduebound. pfa_gap_division_degree_executionquotientsteppreviousresiduebound + S (pfd_previous_division_degree_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_division_degree_executionquotientsteppreviousresiduecongruence pfa_offset_right_division_degree_executionquotientsteppreviousresiduecongruence. (pfc_natural_sum_division_degree_executionquotientstepprevious) + (p) * pfa_offset_left_division_degree_executionquotientsteppreviousresiduecongruence = (pfd_previous_division_degree_executionquotientstep) + (p) * pfa_offset_right_division_degree_executionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_degree_executionquotientstepsubtractleft. pfa_gap_division_degree_executionquotientstepsubtractleft + S (pfd_previous_division_degree_executionquotientstep) = (p)) /\ (((exists pfa_gap_division_degree_executionquotientstepsubtractright. pfa_gap_division_degree_executionquotientstepsubtractright + S (pfd_difference_division_degree_executionquotientstep) = (p)) /\ ((((exists pfa_gap_division_degree_executionquotientstepsubtractresultbound. pfa_gap_division_degree_executionquotientstepsubtractresultbound + S (pfd_input_division_degree_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_division_degree_executionquotientstepsubtractresultcongruence pfa_offset_right_division_degree_executionquotientstepsubtractresultcongruence. ((pfd_previous_division_degree_executionquotientstep) + (pfd_difference_division_degree_executionquotientstep)) + (p) * pfa_offset_left_division_degree_executionquotientstepsubtractresultcongruence = (pfd_input_division_degree_executionquotientstep) + (p) * pfa_offset_right_division_degree_executionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_degree_executionquotientstepmultiplyleft. pfa_gap_division_degree_executionquotientstepmultiplyleft + S (pfd_inverse_division_degree_execution) = (p)) /\ (((exists pfa_gap_division_degree_executionquotientstepmultiplyright. pfa_gap_division_degree_executionquotientstepmultiplyright + S (pfd_difference_division_degree_executionquotientstep) = (p)) /\ ((((exists pfa_gap_division_degree_executionquotientstepmultiplyresultbound. pfa_gap_division_degree_executionquotientstepmultiplyresultbound + S (pfd_value_division_degree_executionquotient) = (p)) /\ ((exists pfa_offset_left_division_degree_executionquotientstepmultiplyresultcongruence pfa_offset_right_division_degree_executionquotientstepmultiplyresultcongruence. ((pfd_inverse_division_degree_execution) * (pfd_difference_division_degree_executionquotientstep)) + (p) * pfa_offset_left_division_degree_executionquotientstepmultiplyresultcongruence = (pfd_value_division_degree_executionquotient) + (p) * pfa_offset_right_division_degree_executionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_division_degree_executionproduct. (exists pfa_gap_division_degree_executionproductbound. pfa_gap_division_degree_executionproductbound + S (pfc_index_division_degree_executionproduct) = (L)) -> exists pfc_value_division_degree_executionproduct. ((((exists ff_h_pfp_division_degree_executionproductentry. ff_h_pfp_division_degree_executionproductentry + S (pfc_value_division_degree_executionproduct) = S ((S (pfc_index_division_degree_executionproduct)) * pfd_product_scale_division_degree_execution)) /\ exists ff_q_pfp_division_degree_executionproductentry. pfd_product_code_division_degree_execution = ff_q_pfp_division_degree_executionproductentry * S ((S (pfc_index_division_degree_executionproduct)) * pfd_product_scale_division_degree_execution) + (pfc_value_division_degree_executionproduct))) /\ ((exists pfc_terms_code_division_degree_executionproductcoefficient pfc_terms_scale_division_degree_executionproductcoefficient pfc_natural_sum_division_degree_executionproductcoefficient. ((forall pfc_index_division_degree_executionproductcoefficientdiagonal. (exists pfa_gap_division_degree_executionproductcoefficientdiagonalbound. pfa_gap_division_degree_executionproductcoefficientdiagonalbound + S (pfc_index_division_degree_executionproductcoefficientdiagonal) = (S (pfc_index_division_degree_executionproduct))) -> exists pfc_value_division_degree_executionproductcoefficientdiagonal. ((((exists ff_h_pfp_division_degree_executionproductcoefficientdiagonalentry. ff_h_pfp_division_degree_executionproductcoefficientdiagonalentry + S (pfc_value_division_degree_executionproductcoefficientdiagonal) = S ((S (pfc_index_division_degree_executionproductcoefficientdiagonal)) * pfc_terms_scale_division_degree_executionproductcoefficient)) /\ exists ff_q_pfp_division_degree_executionproductcoefficientdiagonalentry. pfc_terms_code_division_degree_executionproductcoefficient = ff_q_pfp_division_degree_executionproductcoefficientdiagonalentry * S ((S (pfc_index_division_degree_executionproductcoefficientdiagonal)) * pfc_terms_scale_division_degree_executionproductcoefficient) + (pfc_value_division_degree_executionproductcoefficientdiagonal))) /\ ((exists pfc_complement_division_degree_executionproductcoefficientdiagonalterm pfc_left_division_degree_executionproductcoefficientdiagonalterm pfc_right_division_degree_executionproductcoefficientdiagonalterm. (((pfc_index_division_degree_executionproductcoefficientdiagonal)+pfc_complement_division_degree_executionproductcoefficientdiagonalterm=(pfc_index_division_degree_executionproduct)) /\ ((((((exists pfa_gap_division_degree_executionproductcoefficientdiagonaltermleftinside. pfa_gap_division_degree_executionproductcoefficientdiagonaltermleftinside + S (pfc_index_division_degree_executionproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_degree_executionproductcoefficientdiagonaltermleftentry. ff_h_pfp_division_degree_executionproductcoefficientdiagonaltermleftentry + S (pfc_left_division_degree_executionproductcoefficientdiagonalterm) = S ((S (pfc_index_division_degree_executionproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_degree_executionproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_degree_executionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_degree_executionproductcoefficientdiagonal)) * qc) + (pfc_left_division_degree_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_degree_executionproductcoefficientdiagonaltermleftoutside. pfc_gap_division_degree_executionproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_degree_executionproductcoefficientdiagonal)) /\ (((pfc_left_division_degree_executionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_degree_executionproductcoefficientdiagonaltermrightinside. pfa_gap_division_degree_executionproductcoefficientdiagonaltermrightinside + S (pfc_complement_division_degree_executionproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_degree_executionproductcoefficientdiagonaltermrightentry. ff_h_pfp_division_degree_executionproductcoefficientdiagonaltermrightentry + S (pfc_right_division_degree_executionproductcoefficientdiagonalterm) = S ((S (pfc_complement_division_degree_executionproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_degree_executionproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_degree_executionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_degree_executionproductcoefficientdiagonalterm)) * bc) + (pfc_right_division_degree_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_degree_executionproductcoefficientdiagonaltermrightoutside. pfc_gap_division_degree_executionproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_degree_executionproductcoefficientdiagonalterm)) /\ (((pfc_right_division_degree_executionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_degree_executionproductcoefficientdiagonal)=pfc_left_division_degree_executionproductcoefficientdiagonalterm*pfc_right_division_degree_executionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_degree_executionproductcoefficientsum fs_v_pfc_division_degree_executionproductcoefficientsum. ((((exists fs_h_pfc_division_degree_executionproductcoefficientsum_body_start. fs_h_pfc_division_degree_executionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_degree_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_degree_executionproductcoefficientsum_body_start. fs_u_pfc_division_degree_executionproductcoefficientsum = fs_q_pfc_division_degree_executionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_degree_executionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_degree_executionproductcoefficientsum_body_terminal. fs_h_pfc_division_degree_executionproductcoefficientsum_body_terminal + S (pfc_natural_sum_division_degree_executionproductcoefficient) = S ((S (S (pfc_index_division_degree_executionproduct))) * fs_v_pfc_division_degree_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_degree_executionproductcoefficientsum_body_terminal. fs_u_pfc_division_degree_executionproductcoefficientsum = fs_q_pfc_division_degree_executionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_division_degree_executionproduct))) * fs_v_pfc_division_degree_executionproductcoefficientsum) + (pfc_natural_sum_division_degree_executionproductcoefficient))) /\ forall fs_i_pfc_division_degree_executionproductcoefficientsum_body_steps. (exists fs_lt_pfc_division_degree_executionproductcoefficientsum_body_steps_bound. fs_lt_pfc_division_degree_executionproductcoefficientsum_body_steps_bound + S fs_i_pfc_division_degree_executionproductcoefficientsum_body_steps = S (pfc_index_division_degree_executionproduct)) -> exists fs_a_pfc_division_degree_executionproductcoefficientsum_body_steps fs_r_pfc_division_degree_executionproductcoefficientsum_body_steps fs_s_pfc_division_degree_executionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_division_degree_executionproductcoefficientsum_body_steps_summand. fs_h_pfc_division_degree_executionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_division_degree_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_degree_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_division_degree_executionproductcoefficient)) /\ exists fs_q_pfc_division_degree_executionproductcoefficientsum_body_steps_summand. pfc_terms_code_division_degree_executionproductcoefficient = fs_q_pfc_division_degree_executionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_degree_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_division_degree_executionproductcoefficient) + (fs_a_pfc_division_degree_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_degree_executionproductcoefficientsum_body_steps_partial. fs_h_pfc_division_degree_executionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_division_degree_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_degree_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_degree_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_degree_executionproductcoefficientsum_body_steps_partial. fs_u_pfc_division_degree_executionproductcoefficientsum = fs_q_pfc_division_degree_executionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_degree_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_degree_executionproductcoefficientsum) + (fs_r_pfc_division_degree_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_degree_executionproductcoefficientsum_body_steps_successor. fs_h_pfc_division_degree_executionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_division_degree_executionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_degree_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_degree_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_degree_executionproductcoefficientsum_body_steps_successor. fs_u_pfc_division_degree_executionproductcoefficientsum = fs_q_pfc_division_degree_executionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_degree_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_degree_executionproductcoefficientsum) + (fs_s_pfc_division_degree_executionproductcoefficientsum_body_steps))) /\ fs_s_pfc_division_degree_executionproductcoefficientsum_body_steps = fs_r_pfc_division_degree_executionproductcoefficientsum_body_steps + fs_a_pfc_division_degree_executionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_degree_executionproductcoefficientresiduebound. pfa_gap_division_degree_executionproductcoefficientresiduebound + S (pfc_value_division_degree_executionproduct) = (p)) /\ ((exists pfa_offset_left_division_degree_executionproductcoefficientresiduecongruence pfa_offset_right_division_degree_executionproductcoefficientresiduecongruence. (pfc_natural_sum_division_degree_executionproductcoefficient) + (p) * pfa_offset_left_division_degree_executionproductcoefficientresiduecongruence = (pfc_value_division_degree_executionproduct) + (p) * pfa_offset_right_division_degree_executionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_division_degree_executiondifference. (exists pfa_gap_division_degree_executiondifferenceindex. pfa_gap_division_degree_executiondifferenceindex + S (pfs_index_division_degree_executiondifference) = (L)) -> exists pfs_left_division_degree_executiondifference pfs_right_division_degree_executiondifference pfs_result_division_degree_executiondifference. ((((exists ff_h_pfp_division_degree_executiondifferenceleft. ff_h_pfp_division_degree_executiondifferenceleft + S (pfs_left_division_degree_executiondifference) = S ((S (pfs_index_division_degree_executiondifference)) * ac)) /\ exists ff_q_pfp_division_degree_executiondifferenceleft. ab = ff_q_pfp_division_degree_executiondifferenceleft * S ((S (pfs_index_division_degree_executiondifference)) * ac) + (pfs_left_division_degree_executiondifference))) /\ (((((exists ff_h_pfp_division_degree_executiondifferenceright. ff_h_pfp_division_degree_executiondifferenceright + S (pfs_right_division_degree_executiondifference) = S ((S (pfs_index_division_degree_executiondifference)) * pfd_product_scale_division_degree_execution)) /\ exists ff_q_pfp_division_degree_executiondifferenceright. pfd_product_code_division_degree_execution = ff_q_pfp_division_degree_executiondifferenceright * S ((S (pfs_index_division_degree_executiondifference)) * pfd_product_scale_division_degree_execution) + (pfs_right_division_degree_executiondifference))) /\ (((((exists ff_h_pfp_division_degree_executiondifferenceresult. ff_h_pfp_division_degree_executiondifferenceresult + S (pfs_result_division_degree_executiondifference) = S ((S (pfs_index_division_degree_executiondifference)) * pfd_residual_scale_division_degree_execution)) /\ exists ff_q_pfp_division_degree_executiondifferenceresult. pfd_residual_code_division_degree_execution = ff_q_pfp_division_degree_executiondifferenceresult * S ((S (pfs_index_division_degree_executiondifference)) * pfd_residual_scale_division_degree_execution) + (pfs_result_division_degree_executiondifference))) /\ ((((exists pfa_gap_division_degree_executiondifferenceoperationleft. pfa_gap_division_degree_executiondifferenceoperationleft + S (pfs_right_division_degree_executiondifference) = (p)) /\ (((exists pfa_gap_division_degree_executiondifferenceoperationright. pfa_gap_division_degree_executiondifferenceoperationright + S (pfs_result_division_degree_executiondifference) = (p)) /\ ((((exists pfa_gap_division_degree_executiondifferenceoperationresultbound. pfa_gap_division_degree_executiondifferenceoperationresultbound + S (pfs_left_division_degree_executiondifference) = (p)) /\ ((exists pfa_offset_left_division_degree_executiondifferenceoperationresultcongruence pfa_offset_right_division_degree_executiondifferenceoperationresultcongruence. ((pfs_right_division_degree_executiondifference) + (pfs_result_division_degree_executiondifference)) + (p) * pfa_offset_left_division_degree_executiondifferenceoperationresultcongruence = (pfs_left_division_degree_executiondifference) + (p) * pfa_offset_right_division_degree_executiondifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_division_degree_execution)+(R)) /\ (((forall fom_index_pfp_division_degree_executiontriminput. (exists fom_gap_pfp_division_degree_executiontriminput_index_bound. fom_gap_pfp_division_degree_executiontriminput_index_bound + S (fom_index_pfp_division_degree_executiontriminput) = L) -> exists fom_value_pfp_division_degree_executiontriminput. ((((exists fom_beta_height_pfp_division_degree_executiontriminput_entry. fom_beta_height_pfp_division_degree_executiontriminput_entry + S (fom_value_pfp_division_degree_executiontriminput) = S ((S (fom_index_pfp_division_degree_executiontriminput)) * pfd_residual_scale_division_degree_execution)) /\ exists fom_beta_quotient_pfp_division_degree_executiontriminput_entry. pfd_residual_code_division_degree_execution = fom_beta_quotient_pfp_division_degree_executiontriminput_entry * S ((S (fom_index_pfp_division_degree_executiontriminput)) * pfd_residual_scale_division_degree_execution) + (fom_value_pfp_division_degree_executiontriminput))) /\ (exists fom_gap_pfp_division_degree_executiontriminput_value_bound. fom_gap_pfp_division_degree_executiontriminput_value_bound + S (fom_value_pfp_division_degree_executiontriminput) = p))) /\ (((forall pfp_repeat_index_division_degree_executiontrimremoved. (exists pfa_gap_division_degree_executiontrimremovedindex. pfa_gap_division_degree_executiontrimremovedindex + S (pfp_repeat_index_division_degree_executiontrimremoved) = (pfd_cut_division_degree_execution)) -> (((exists ff_h_pfp_division_degree_executiontrimremovedentry. ff_h_pfp_division_degree_executiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_division_degree_executiontrimremoved)) * pfd_residual_scale_division_degree_execution)) /\ exists ff_q_pfp_division_degree_executiontrimremovedentry. pfd_residual_code_division_degree_execution = ff_q_pfp_division_degree_executiontrimremovedentry * S ((S (pfp_repeat_index_division_degree_executiontrimremoved)) * pfd_residual_scale_division_degree_execution) + (0)))) /\ (((forall pftrim_index_division_degree_executiontrimsuffix pftrim_value_division_degree_executiontrimsuffix. (exists pfa_gap_division_degree_executiontrimsuffixbound. pfa_gap_division_degree_executiontrimsuffixbound + S (pftrim_index_division_degree_executiontrimsuffix) = (R)) -> (((exists ff_h_pfp_division_degree_executiontrimsuffixsource. ff_h_pfp_division_degree_executiontrimsuffixsource + S (pftrim_value_division_degree_executiontrimsuffix) = S ((S ((pfd_cut_division_degree_execution)+pftrim_index_division_degree_executiontrimsuffix)) * pfd_residual_scale_division_degree_execution)) /\ exists ff_q_pfp_division_degree_executiontrimsuffixsource. pfd_residual_code_division_degree_execution = ff_q_pfp_division_degree_executiontrimsuffixsource * S ((S ((pfd_cut_division_degree_execution)+pftrim_index_division_degree_executiontrimsuffix)) * pfd_residual_scale_division_degree_execution) + (pftrim_value_division_degree_executiontrimsuffix))) -> (((exists ff_h_pfp_division_degree_executiontrimsuffixoutput. ff_h_pfp_division_degree_executiontrimsuffixoutput + S (pftrim_value_division_degree_executiontrimsuffix) = S ((S (pftrim_index_division_degree_executiontrimsuffix)) * rc)) /\ exists ff_q_pfp_division_degree_executiontrimsuffixoutput. rb = ff_q_pfp_division_degree_executiontrimsuffixoutput * S ((S (pftrim_index_division_degree_executiontrimsuffix)) * rc) + (pftrim_value_division_degree_executiontrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_degree_executiontrimnormal. ((((exists ff_h_pfp_division_degree_executiontrimnormalentry. ff_h_pfp_division_degree_executiontrimnormalentry + S (pftrim_leading_division_degree_executiontrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_degree_executiontrimnormalentry. rb = ff_q_pfp_division_degree_executiontrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_degree_executiontrimnormal))) /\ ((~(pftrim_leading_division_degree_executiontrimnormal=0))))))))))))))))))))))))))))))))) -> ((R)=0 \/ (exists pfd_remainder_degree_division_degree_result. (((((R)=S (pfd_remainder_degree_division_degree_result)) /\ (((forall fom_index_pfp_division_degree_resultrepresentedcoefficients. (exists fom_gap_pfp_division_degree_resultrepresentedcoefficients_index_bound. fom_gap_pfp_division_degree_resultrepresentedcoefficients_index_bound + S (fom_index_pfp_division_degree_resultrepresentedcoefficients) = R) -> exists fom_value_pfp_division_degree_resultrepresentedcoefficients. ((((exists fom_beta_height_pfp_division_degree_resultrepresentedcoefficients_entry. fom_beta_height_pfp_division_degree_resultrepresentedcoefficients_entry + S (fom_value_pfp_division_degree_resultrepresentedcoefficients) = S ((S (fom_index_pfp_division_degree_resultrepresentedcoefficients)) * rc)) /\ exists fom_beta_quotient_pfp_division_degree_resultrepresentedcoefficients_entry. rb = fom_beta_quotient_pfp_division_degree_resultrepresentedcoefficients_entry * S ((S (fom_index_pfp_division_degree_resultrepresentedcoefficients)) * rc) + (fom_value_pfp_division_degree_resultrepresentedcoefficients))) /\ (exists fom_gap_pfp_division_degree_resultrepresentedcoefficients_value_bound. fom_gap_pfp_division_degree_resultrepresentedcoefficients_value_bound + S (fom_value_pfp_division_degree_resultrepresentedcoefficients) = p))) /\ ((exists pfd_leading_division_degree_resultrepresented. ((((exists ff_h_pfp_division_degree_resultrepresentedentry. ff_h_pfp_division_degree_resultrepresentedentry + S (pfd_leading_division_degree_resultrepresented) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_degree_resultrepresentedentry. rb = ff_q_pfp_division_degree_resultrepresentedentry * S ((S (0)) * rc) + (pfd_leading_division_degree_resultrepresented))) /\ ((~(pfd_leading_division_degree_resultrepresented=0)))))))))) /\ ((exists pfa_gap_division_degree_resultstrict. pfa_gap_division_degree_resultstrict + S (pfd_remainder_degree_division_degree_result) = (d))))))