prime_field_polynomial_division_coefficient_identity

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_identity_prime pfa_factor_right_division_identity_prime. (p) = pfa_factor_left_division_identity_prime * pfa_factor_right_division_identity_prime -> pfa_factor_left_division_identity_prime = 1 \/ pfa_factor_right_division_identity_prime = 1) -> (((forall fom_index_pfp_division_identity_executioninput. (exists fom_gap_pfp_division_identity_executioninput_index_bound. fom_gap_pfp_division_identity_executioninput_index_bound + S (fom_index_pfp_division_identity_executioninput) = L) -> exists fom_value_pfp_division_identity_executioninput. ((((exists fom_beta_height_pfp_division_identity_executioninput_entry. fom_beta_height_pfp_division_identity_executioninput_entry + S (fom_value_pfp_division_identity_executioninput) = S ((S (fom_index_pfp_division_identity_executioninput)) * ac)) /\ exists fom_beta_quotient_pfp_division_identity_executioninput_entry. ab = fom_beta_quotient_pfp_division_identity_executioninput_entry * S ((S (fom_index_pfp_division_identity_executioninput)) * ac) + (fom_value_pfp_division_identity_executioninput))) /\ (exists fom_gap_pfp_division_identity_executioninput_value_bound. fom_gap_pfp_division_identity_executioninput_value_bound + S (fom_value_pfp_division_identity_executioninput) = p))) /\ (((forall fom_index_pfp_division_identity_executiondivisor. (exists fom_gap_pfp_division_identity_executiondivisor_index_bound. fom_gap_pfp_division_identity_executiondivisor_index_bound + S (fom_index_pfp_division_identity_executiondivisor) = S (d)) -> exists fom_value_pfp_division_identity_executiondivisor. ((((exists fom_beta_height_pfp_division_identity_executiondivisor_entry. fom_beta_height_pfp_division_identity_executiondivisor_entry + S (fom_value_pfp_division_identity_executiondivisor) = S ((S (fom_index_pfp_division_identity_executiondivisor)) * bc)) /\ exists fom_beta_quotient_pfp_division_identity_executiondivisor_entry. bb = fom_beta_quotient_pfp_division_identity_executiondivisor_entry * S ((S (fom_index_pfp_division_identity_executiondivisor)) * bc) + (fom_value_pfp_division_identity_executiondivisor))) /\ (exists fom_gap_pfp_division_identity_executiondivisor_value_bound. fom_gap_pfp_division_identity_executiondivisor_value_bound + S (fom_value_pfp_division_identity_executiondivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_division_identity_executionlengthshort. pfc_gap_division_identity_executionlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_division_identity_execution pfd_inverse_division_identity_execution pfd_product_code_division_identity_execution pfd_product_scale_division_identity_execution pfd_residual_code_division_identity_execution pfd_residual_scale_division_identity_execution pfd_cut_division_identity_execution. ((((exists ff_h_pfp_division_identity_executionhead. ff_h_pfp_division_identity_executionhead + S (pfd_head_division_identity_execution) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_identity_executionhead. bb = ff_q_pfp_division_identity_executionhead * S ((S (0)) * bc) + (pfd_head_division_identity_execution))) /\ (((((~((pfd_head_division_identity_execution) = 0)) /\ ((((exists pfa_gap_division_identity_executioninversemultiplicationleft. pfa_gap_division_identity_executioninversemultiplicationleft + S (pfd_head_division_identity_execution) = (p)) /\ (((exists pfa_gap_division_identity_executioninversemultiplicationright. pfa_gap_division_identity_executioninversemultiplicationright + S (pfd_inverse_division_identity_execution) = (p)) /\ ((((exists pfa_gap_division_identity_executioninversemultiplicationresultbound. pfa_gap_division_identity_executioninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_identity_executioninversemultiplicationresultcongruence pfa_offset_right_division_identity_executioninversemultiplicationresultcongruence. ((pfd_head_division_identity_execution) * (pfd_inverse_division_identity_execution)) + (p) * pfa_offset_left_division_identity_executioninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_identity_executioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_division_identity_executionquotient. (exists pfa_gap_division_identity_executionquotientbound. pfa_gap_division_identity_executionquotientbound + S (pfd_index_division_identity_executionquotient) = (q)) -> exists pfd_value_division_identity_executionquotient. ((((exists ff_h_pfp_division_identity_executionquotiententry. ff_h_pfp_division_identity_executionquotiententry + S (pfd_value_division_identity_executionquotient) = S ((S (pfd_index_division_identity_executionquotient)) * qc)) /\ exists ff_q_pfp_division_identity_executionquotiententry. qb = ff_q_pfp_division_identity_executionquotiententry * S ((S (pfd_index_division_identity_executionquotient)) * qc) + (pfd_value_division_identity_executionquotient))) /\ ((exists pfd_input_division_identity_executionquotientstep pfd_previous_division_identity_executionquotientstep pfd_difference_division_identity_executionquotientstep. ((((exists ff_h_pfp_division_identity_executionquotientstepinput. ff_h_pfp_division_identity_executionquotientstepinput + S (pfd_input_division_identity_executionquotientstep) = S ((S (pfd_index_division_identity_executionquotient)) * ac)) /\ exists ff_q_pfp_division_identity_executionquotientstepinput. ab = ff_q_pfp_division_identity_executionquotientstepinput * S ((S (pfd_index_division_identity_executionquotient)) * ac) + (pfd_input_division_identity_executionquotientstep))) /\ (((exists pfc_terms_code_division_identity_executionquotientstepprevious pfc_terms_scale_division_identity_executionquotientstepprevious pfc_natural_sum_division_identity_executionquotientstepprevious. ((forall pfc_index_division_identity_executionquotientsteppreviousdiagonal. (exists pfa_gap_division_identity_executionquotientsteppreviousdiagonalbound. pfa_gap_division_identity_executionquotientsteppreviousdiagonalbound + S (pfc_index_division_identity_executionquotientsteppreviousdiagonal) = (S (pfd_index_division_identity_executionquotient))) -> exists pfc_value_division_identity_executionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_division_identity_executionquotientsteppreviousdiagonalentry. ff_h_pfp_division_identity_executionquotientsteppreviousdiagonalentry + S (pfc_value_division_identity_executionquotientsteppreviousdiagonal) = S ((S (pfc_index_division_identity_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_division_identity_executionquotientstepprevious)) /\ exists ff_q_pfp_division_identity_executionquotientsteppreviousdiagonalentry. pfc_terms_code_division_identity_executionquotientstepprevious = ff_q_pfp_division_identity_executionquotientsteppreviousdiagonalentry * S ((S (pfc_index_division_identity_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_division_identity_executionquotientstepprevious) + (pfc_value_division_identity_executionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_division_identity_executionquotientsteppreviousdiagonalterm pfc_left_division_identity_executionquotientsteppreviousdiagonalterm pfc_right_division_identity_executionquotientsteppreviousdiagonalterm. (((pfc_index_division_identity_executionquotientsteppreviousdiagonal)+pfc_complement_division_identity_executionquotientsteppreviousdiagonalterm=(pfd_index_division_identity_executionquotient)) /\ ((((((exists pfa_gap_division_identity_executionquotientsteppreviousdiagonaltermleftinside. pfa_gap_division_identity_executionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_division_identity_executionquotientsteppreviousdiagonal) = (pfd_index_division_identity_executionquotient)) /\ ((((exists ff_h_pfp_division_identity_executionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_division_identity_executionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_division_identity_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_division_identity_executionquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_identity_executionquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_identity_executionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_identity_executionquotientsteppreviousdiagonal)) * qc) + (pfc_left_division_identity_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_identity_executionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_division_identity_executionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_division_identity_executionquotient)=(pfc_index_division_identity_executionquotientsteppreviousdiagonal)) /\ (((pfc_left_division_identity_executionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_identity_executionquotientsteppreviousdiagonaltermrightinside. pfa_gap_division_identity_executionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_division_identity_executionquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_identity_executionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_division_identity_executionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_division_identity_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_division_identity_executionquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_identity_executionquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_identity_executionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_identity_executionquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_division_identity_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_identity_executionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_division_identity_executionquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_division_identity_executionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_division_identity_executionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_identity_executionquotientsteppreviousdiagonal)=pfc_left_division_identity_executionquotientsteppreviousdiagonalterm*pfc_right_division_identity_executionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_identity_executionquotientstepprevioussum fs_v_pfc_division_identity_executionquotientstepprevioussum. ((((exists fs_h_pfc_division_identity_executionquotientstepprevioussum_body_start. fs_h_pfc_division_identity_executionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_identity_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_identity_executionquotientstepprevioussum_body_start. fs_u_pfc_division_identity_executionquotientstepprevioussum = fs_q_pfc_division_identity_executionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_identity_executionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_identity_executionquotientstepprevioussum_body_terminal. fs_h_pfc_division_identity_executionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_division_identity_executionquotientstepprevious) = S ((S (S (pfd_index_division_identity_executionquotient))) * fs_v_pfc_division_identity_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_identity_executionquotientstepprevioussum_body_terminal. fs_u_pfc_division_identity_executionquotientstepprevioussum = fs_q_pfc_division_identity_executionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_division_identity_executionquotient))) * fs_v_pfc_division_identity_executionquotientstepprevioussum) + (pfc_natural_sum_division_identity_executionquotientstepprevious))) /\ forall fs_i_pfc_division_identity_executionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_division_identity_executionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_division_identity_executionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_division_identity_executionquotientstepprevioussum_body_steps = S (pfd_index_division_identity_executionquotient)) -> exists fs_a_pfc_division_identity_executionquotientstepprevioussum_body_steps fs_r_pfc_division_identity_executionquotientstepprevioussum_body_steps fs_s_pfc_division_identity_executionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_division_identity_executionquotientstepprevioussum_body_steps_summand. fs_h_pfc_division_identity_executionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_division_identity_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_identity_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_identity_executionquotientstepprevious)) /\ exists fs_q_pfc_division_identity_executionquotientstepprevioussum_body_steps_summand. pfc_terms_code_division_identity_executionquotientstepprevious = fs_q_pfc_division_identity_executionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_identity_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_identity_executionquotientstepprevious) + (fs_a_pfc_division_identity_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_identity_executionquotientstepprevioussum_body_steps_partial. fs_h_pfc_division_identity_executionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_division_identity_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_identity_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_identity_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_identity_executionquotientstepprevioussum_body_steps_partial. fs_u_pfc_division_identity_executionquotientstepprevioussum = fs_q_pfc_division_identity_executionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_identity_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_identity_executionquotientstepprevioussum) + (fs_r_pfc_division_identity_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_identity_executionquotientstepprevioussum_body_steps_successor. fs_h_pfc_division_identity_executionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_division_identity_executionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_identity_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_identity_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_identity_executionquotientstepprevioussum_body_steps_successor. fs_u_pfc_division_identity_executionquotientstepprevioussum = fs_q_pfc_division_identity_executionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_identity_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_identity_executionquotientstepprevioussum) + (fs_s_pfc_division_identity_executionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_division_identity_executionquotientstepprevioussum_body_steps = fs_r_pfc_division_identity_executionquotientstepprevioussum_body_steps + fs_a_pfc_division_identity_executionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_identity_executionquotientsteppreviousresiduebound. pfa_gap_division_identity_executionquotientsteppreviousresiduebound + S (pfd_previous_division_identity_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_division_identity_executionquotientsteppreviousresiduecongruence pfa_offset_right_division_identity_executionquotientsteppreviousresiduecongruence. (pfc_natural_sum_division_identity_executionquotientstepprevious) + (p) * pfa_offset_left_division_identity_executionquotientsteppreviousresiduecongruence = (pfd_previous_division_identity_executionquotientstep) + (p) * pfa_offset_right_division_identity_executionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_identity_executionquotientstepsubtractleft. pfa_gap_division_identity_executionquotientstepsubtractleft + S (pfd_previous_division_identity_executionquotientstep) = (p)) /\ (((exists pfa_gap_division_identity_executionquotientstepsubtractright. pfa_gap_division_identity_executionquotientstepsubtractright + S (pfd_difference_division_identity_executionquotientstep) = (p)) /\ ((((exists pfa_gap_division_identity_executionquotientstepsubtractresultbound. pfa_gap_division_identity_executionquotientstepsubtractresultbound + S (pfd_input_division_identity_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_division_identity_executionquotientstepsubtractresultcongruence pfa_offset_right_division_identity_executionquotientstepsubtractresultcongruence. ((pfd_previous_division_identity_executionquotientstep) + (pfd_difference_division_identity_executionquotientstep)) + (p) * pfa_offset_left_division_identity_executionquotientstepsubtractresultcongruence = (pfd_input_division_identity_executionquotientstep) + (p) * pfa_offset_right_division_identity_executionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_identity_executionquotientstepmultiplyleft. pfa_gap_division_identity_executionquotientstepmultiplyleft + S (pfd_inverse_division_identity_execution) = (p)) /\ (((exists pfa_gap_division_identity_executionquotientstepmultiplyright. pfa_gap_division_identity_executionquotientstepmultiplyright + S (pfd_difference_division_identity_executionquotientstep) = (p)) /\ ((((exists pfa_gap_division_identity_executionquotientstepmultiplyresultbound. pfa_gap_division_identity_executionquotientstepmultiplyresultbound + S (pfd_value_division_identity_executionquotient) = (p)) /\ ((exists pfa_offset_left_division_identity_executionquotientstepmultiplyresultcongruence pfa_offset_right_division_identity_executionquotientstepmultiplyresultcongruence. ((pfd_inverse_division_identity_execution) * (pfd_difference_division_identity_executionquotientstep)) + (p) * pfa_offset_left_division_identity_executionquotientstepmultiplyresultcongruence = (pfd_value_division_identity_executionquotient) + (p) * pfa_offset_right_division_identity_executionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_division_identity_executionproduct. (exists pfa_gap_division_identity_executionproductbound. pfa_gap_division_identity_executionproductbound + S (pfc_index_division_identity_executionproduct) = (L)) -> exists pfc_value_division_identity_executionproduct. ((((exists ff_h_pfp_division_identity_executionproductentry. ff_h_pfp_division_identity_executionproductentry + S (pfc_value_division_identity_executionproduct) = S ((S (pfc_index_division_identity_executionproduct)) * pfd_product_scale_division_identity_execution)) /\ exists ff_q_pfp_division_identity_executionproductentry. pfd_product_code_division_identity_execution = ff_q_pfp_division_identity_executionproductentry * S ((S (pfc_index_division_identity_executionproduct)) * pfd_product_scale_division_identity_execution) + (pfc_value_division_identity_executionproduct))) /\ ((exists pfc_terms_code_division_identity_executionproductcoefficient pfc_terms_scale_division_identity_executionproductcoefficient pfc_natural_sum_division_identity_executionproductcoefficient. ((forall pfc_index_division_identity_executionproductcoefficientdiagonal. (exists pfa_gap_division_identity_executionproductcoefficientdiagonalbound. pfa_gap_division_identity_executionproductcoefficientdiagonalbound + S (pfc_index_division_identity_executionproductcoefficientdiagonal) = (S (pfc_index_division_identity_executionproduct))) -> exists pfc_value_division_identity_executionproductcoefficientdiagonal. ((((exists ff_h_pfp_division_identity_executionproductcoefficientdiagonalentry. ff_h_pfp_division_identity_executionproductcoefficientdiagonalentry + S (pfc_value_division_identity_executionproductcoefficientdiagonal) = S ((S (pfc_index_division_identity_executionproductcoefficientdiagonal)) * pfc_terms_scale_division_identity_executionproductcoefficient)) /\ exists ff_q_pfp_division_identity_executionproductcoefficientdiagonalentry. pfc_terms_code_division_identity_executionproductcoefficient = ff_q_pfp_division_identity_executionproductcoefficientdiagonalentry * S ((S (pfc_index_division_identity_executionproductcoefficientdiagonal)) * pfc_terms_scale_division_identity_executionproductcoefficient) + (pfc_value_division_identity_executionproductcoefficientdiagonal))) /\ ((exists pfc_complement_division_identity_executionproductcoefficientdiagonalterm pfc_left_division_identity_executionproductcoefficientdiagonalterm pfc_right_division_identity_executionproductcoefficientdiagonalterm. (((pfc_index_division_identity_executionproductcoefficientdiagonal)+pfc_complement_division_identity_executionproductcoefficientdiagonalterm=(pfc_index_division_identity_executionproduct)) /\ ((((((exists pfa_gap_division_identity_executionproductcoefficientdiagonaltermleftinside. pfa_gap_division_identity_executionproductcoefficientdiagonaltermleftinside + S (pfc_index_division_identity_executionproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_identity_executionproductcoefficientdiagonaltermleftentry. ff_h_pfp_division_identity_executionproductcoefficientdiagonaltermleftentry + S (pfc_left_division_identity_executionproductcoefficientdiagonalterm) = S ((S (pfc_index_division_identity_executionproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_identity_executionproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_identity_executionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_identity_executionproductcoefficientdiagonal)) * qc) + (pfc_left_division_identity_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_identity_executionproductcoefficientdiagonaltermleftoutside. pfc_gap_division_identity_executionproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_identity_executionproductcoefficientdiagonal)) /\ (((pfc_left_division_identity_executionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_identity_executionproductcoefficientdiagonaltermrightinside. pfa_gap_division_identity_executionproductcoefficientdiagonaltermrightinside + S (pfc_complement_division_identity_executionproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_identity_executionproductcoefficientdiagonaltermrightentry. ff_h_pfp_division_identity_executionproductcoefficientdiagonaltermrightentry + S (pfc_right_division_identity_executionproductcoefficientdiagonalterm) = S ((S (pfc_complement_division_identity_executionproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_identity_executionproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_identity_executionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_identity_executionproductcoefficientdiagonalterm)) * bc) + (pfc_right_division_identity_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_identity_executionproductcoefficientdiagonaltermrightoutside. pfc_gap_division_identity_executionproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_identity_executionproductcoefficientdiagonalterm)) /\ (((pfc_right_division_identity_executionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_identity_executionproductcoefficientdiagonal)=pfc_left_division_identity_executionproductcoefficientdiagonalterm*pfc_right_division_identity_executionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_identity_executionproductcoefficientsum fs_v_pfc_division_identity_executionproductcoefficientsum. ((((exists fs_h_pfc_division_identity_executionproductcoefficientsum_body_start. fs_h_pfc_division_identity_executionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_identity_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_identity_executionproductcoefficientsum_body_start. fs_u_pfc_division_identity_executionproductcoefficientsum = fs_q_pfc_division_identity_executionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_identity_executionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_identity_executionproductcoefficientsum_body_terminal. fs_h_pfc_division_identity_executionproductcoefficientsum_body_terminal + S (pfc_natural_sum_division_identity_executionproductcoefficient) = S ((S (S (pfc_index_division_identity_executionproduct))) * fs_v_pfc_division_identity_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_identity_executionproductcoefficientsum_body_terminal. fs_u_pfc_division_identity_executionproductcoefficientsum = fs_q_pfc_division_identity_executionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_division_identity_executionproduct))) * fs_v_pfc_division_identity_executionproductcoefficientsum) + (pfc_natural_sum_division_identity_executionproductcoefficient))) /\ forall fs_i_pfc_division_identity_executionproductcoefficientsum_body_steps. (exists fs_lt_pfc_division_identity_executionproductcoefficientsum_body_steps_bound. fs_lt_pfc_division_identity_executionproductcoefficientsum_body_steps_bound + S fs_i_pfc_division_identity_executionproductcoefficientsum_body_steps = S (pfc_index_division_identity_executionproduct)) -> exists fs_a_pfc_division_identity_executionproductcoefficientsum_body_steps fs_r_pfc_division_identity_executionproductcoefficientsum_body_steps fs_s_pfc_division_identity_executionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_division_identity_executionproductcoefficientsum_body_steps_summand. fs_h_pfc_division_identity_executionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_division_identity_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_identity_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_division_identity_executionproductcoefficient)) /\ exists fs_q_pfc_division_identity_executionproductcoefficientsum_body_steps_summand. pfc_terms_code_division_identity_executionproductcoefficient = fs_q_pfc_division_identity_executionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_identity_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_division_identity_executionproductcoefficient) + (fs_a_pfc_division_identity_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_identity_executionproductcoefficientsum_body_steps_partial. fs_h_pfc_division_identity_executionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_division_identity_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_identity_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_identity_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_identity_executionproductcoefficientsum_body_steps_partial. fs_u_pfc_division_identity_executionproductcoefficientsum = fs_q_pfc_division_identity_executionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_identity_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_identity_executionproductcoefficientsum) + (fs_r_pfc_division_identity_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_identity_executionproductcoefficientsum_body_steps_successor. fs_h_pfc_division_identity_executionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_division_identity_executionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_identity_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_identity_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_identity_executionproductcoefficientsum_body_steps_successor. fs_u_pfc_division_identity_executionproductcoefficientsum = fs_q_pfc_division_identity_executionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_identity_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_identity_executionproductcoefficientsum) + (fs_s_pfc_division_identity_executionproductcoefficientsum_body_steps))) /\ fs_s_pfc_division_identity_executionproductcoefficientsum_body_steps = fs_r_pfc_division_identity_executionproductcoefficientsum_body_steps + fs_a_pfc_division_identity_executionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_identity_executionproductcoefficientresiduebound. pfa_gap_division_identity_executionproductcoefficientresiduebound + S (pfc_value_division_identity_executionproduct) = (p)) /\ ((exists pfa_offset_left_division_identity_executionproductcoefficientresiduecongruence pfa_offset_right_division_identity_executionproductcoefficientresiduecongruence. (pfc_natural_sum_division_identity_executionproductcoefficient) + (p) * pfa_offset_left_division_identity_executionproductcoefficientresiduecongruence = (pfc_value_division_identity_executionproduct) + (p) * pfa_offset_right_division_identity_executionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_division_identity_executiondifference. (exists pfa_gap_division_identity_executiondifferenceindex. pfa_gap_division_identity_executiondifferenceindex + S (pfs_index_division_identity_executiondifference) = (L)) -> exists pfs_left_division_identity_executiondifference pfs_right_division_identity_executiondifference pfs_result_division_identity_executiondifference. ((((exists ff_h_pfp_division_identity_executiondifferenceleft. ff_h_pfp_division_identity_executiondifferenceleft + S (pfs_left_division_identity_executiondifference) = S ((S (pfs_index_division_identity_executiondifference)) * ac)) /\ exists ff_q_pfp_division_identity_executiondifferenceleft. ab = ff_q_pfp_division_identity_executiondifferenceleft * S ((S (pfs_index_division_identity_executiondifference)) * ac) + (pfs_left_division_identity_executiondifference))) /\ (((((exists ff_h_pfp_division_identity_executiondifferenceright. ff_h_pfp_division_identity_executiondifferenceright + S (pfs_right_division_identity_executiondifference) = S ((S (pfs_index_division_identity_executiondifference)) * pfd_product_scale_division_identity_execution)) /\ exists ff_q_pfp_division_identity_executiondifferenceright. pfd_product_code_division_identity_execution = ff_q_pfp_division_identity_executiondifferenceright * S ((S (pfs_index_division_identity_executiondifference)) * pfd_product_scale_division_identity_execution) + (pfs_right_division_identity_executiondifference))) /\ (((((exists ff_h_pfp_division_identity_executiondifferenceresult. ff_h_pfp_division_identity_executiondifferenceresult + S (pfs_result_division_identity_executiondifference) = S ((S (pfs_index_division_identity_executiondifference)) * pfd_residual_scale_division_identity_execution)) /\ exists ff_q_pfp_division_identity_executiondifferenceresult. pfd_residual_code_division_identity_execution = ff_q_pfp_division_identity_executiondifferenceresult * S ((S (pfs_index_division_identity_executiondifference)) * pfd_residual_scale_division_identity_execution) + (pfs_result_division_identity_executiondifference))) /\ ((((exists pfa_gap_division_identity_executiondifferenceoperationleft. pfa_gap_division_identity_executiondifferenceoperationleft + S (pfs_right_division_identity_executiondifference) = (p)) /\ (((exists pfa_gap_division_identity_executiondifferenceoperationright. pfa_gap_division_identity_executiondifferenceoperationright + S (pfs_result_division_identity_executiondifference) = (p)) /\ ((((exists pfa_gap_division_identity_executiondifferenceoperationresultbound. pfa_gap_division_identity_executiondifferenceoperationresultbound + S (pfs_left_division_identity_executiondifference) = (p)) /\ ((exists pfa_offset_left_division_identity_executiondifferenceoperationresultcongruence pfa_offset_right_division_identity_executiondifferenceoperationresultcongruence. ((pfs_right_division_identity_executiondifference) + (pfs_result_division_identity_executiondifference)) + (p) * pfa_offset_left_division_identity_executiondifferenceoperationresultcongruence = (pfs_left_division_identity_executiondifference) + (p) * pfa_offset_right_division_identity_executiondifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_division_identity_execution)+(R)) /\ (((forall fom_index_pfp_division_identity_executiontriminput. (exists fom_gap_pfp_division_identity_executiontriminput_index_bound. fom_gap_pfp_division_identity_executiontriminput_index_bound + S (fom_index_pfp_division_identity_executiontriminput) = L) -> exists fom_value_pfp_division_identity_executiontriminput. ((((exists fom_beta_height_pfp_division_identity_executiontriminput_entry. fom_beta_height_pfp_division_identity_executiontriminput_entry + S (fom_value_pfp_division_identity_executiontriminput) = S ((S (fom_index_pfp_division_identity_executiontriminput)) * pfd_residual_scale_division_identity_execution)) /\ exists fom_beta_quotient_pfp_division_identity_executiontriminput_entry. pfd_residual_code_division_identity_execution = fom_beta_quotient_pfp_division_identity_executiontriminput_entry * S ((S (fom_index_pfp_division_identity_executiontriminput)) * pfd_residual_scale_division_identity_execution) + (fom_value_pfp_division_identity_executiontriminput))) /\ (exists fom_gap_pfp_division_identity_executiontriminput_value_bound. fom_gap_pfp_division_identity_executiontriminput_value_bound + S (fom_value_pfp_division_identity_executiontriminput) = p))) /\ (((forall pfp_repeat_index_division_identity_executiontrimremoved. (exists pfa_gap_division_identity_executiontrimremovedindex. pfa_gap_division_identity_executiontrimremovedindex + S (pfp_repeat_index_division_identity_executiontrimremoved) = (pfd_cut_division_identity_execution)) -> (((exists ff_h_pfp_division_identity_executiontrimremovedentry. ff_h_pfp_division_identity_executiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_division_identity_executiontrimremoved)) * pfd_residual_scale_division_identity_execution)) /\ exists ff_q_pfp_division_identity_executiontrimremovedentry. pfd_residual_code_division_identity_execution = ff_q_pfp_division_identity_executiontrimremovedentry * S ((S (pfp_repeat_index_division_identity_executiontrimremoved)) * pfd_residual_scale_division_identity_execution) + (0)))) /\ (((forall pftrim_index_division_identity_executiontrimsuffix pftrim_value_division_identity_executiontrimsuffix. (exists pfa_gap_division_identity_executiontrimsuffixbound. pfa_gap_division_identity_executiontrimsuffixbound + S (pftrim_index_division_identity_executiontrimsuffix) = (R)) -> (((exists ff_h_pfp_division_identity_executiontrimsuffixsource. ff_h_pfp_division_identity_executiontrimsuffixsource + S (pftrim_value_division_identity_executiontrimsuffix) = S ((S ((pfd_cut_division_identity_execution)+pftrim_index_division_identity_executiontrimsuffix)) * pfd_residual_scale_division_identity_execution)) /\ exists ff_q_pfp_division_identity_executiontrimsuffixsource. pfd_residual_code_division_identity_execution = ff_q_pfp_division_identity_executiontrimsuffixsource * S ((S ((pfd_cut_division_identity_execution)+pftrim_index_division_identity_executiontrimsuffix)) * pfd_residual_scale_division_identity_execution) + (pftrim_value_division_identity_executiontrimsuffix))) -> (((exists ff_h_pfp_division_identity_executiontrimsuffixoutput. ff_h_pfp_division_identity_executiontrimsuffixoutput + S (pftrim_value_division_identity_executiontrimsuffix) = S ((S (pftrim_index_division_identity_executiontrimsuffix)) * rc)) /\ exists ff_q_pfp_division_identity_executiontrimsuffixoutput. rb = ff_q_pfp_division_identity_executiontrimsuffixoutput * S ((S (pftrim_index_division_identity_executiontrimsuffix)) * rc) + (pftrim_value_division_identity_executiontrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_identity_executiontrimnormal. ((((exists ff_h_pfp_division_identity_executiontrimnormalentry. ff_h_pfp_division_identity_executiontrimnormalentry + S (pftrim_leading_division_identity_executiontrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_identity_executiontrimnormalentry. rb = ff_q_pfp_division_identity_executiontrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_identity_executiontrimnormal))) /\ ((~(pftrim_leading_division_identity_executiontrimnormal=0))))))))))))))))))))))))))))))))) -> (exists pfd_identity_pb_division_identity_result pfd_identity_pc_division_identity_result pfd_identity_ub_division_identity_result pfd_identity_uc_division_identity_result pfd_identity_t_division_identity_result. ((((((q)=0) /\ ((forall pfp_repeat_index_division_identity_resultempty. (exists pfa_gap_division_identity_resultemptyindex. pfa_gap_division_identity_resultemptyindex + S (pfp_repeat_index_division_identity_resultempty) = (L)) -> (((exists ff_h_pfp_division_identity_resultemptyentry. ff_h_pfp_division_identity_resultemptyentry + S (0) = S ((S (pfp_repeat_index_division_identity_resultempty)) * pfd_identity_pc_division_identity_result)) /\ exists ff_q_pfp_division_identity_resultemptyentry. pfd_identity_pb_division_identity_result = ff_q_pfp_division_identity_resultemptyentry * S ((S (pfp_repeat_index_division_identity_resultempty)) * pfd_identity_pc_division_identity_result) + (0))))))) \/ (((~((q)=0)) /\ ((((forall fom_index_pfp_division_identity_resultproductleft. (exists fom_gap_pfp_division_identity_resultproductleft_index_bound. fom_gap_pfp_division_identity_resultproductleft_index_bound + S (fom_index_pfp_division_identity_resultproductleft) = q) -> exists fom_value_pfp_division_identity_resultproductleft. ((((exists fom_beta_height_pfp_division_identity_resultproductleft_entry. fom_beta_height_pfp_division_identity_resultproductleft_entry + S (fom_value_pfp_division_identity_resultproductleft) = S ((S (fom_index_pfp_division_identity_resultproductleft)) * qc)) /\ exists fom_beta_quotient_pfp_division_identity_resultproductleft_entry. qb = fom_beta_quotient_pfp_division_identity_resultproductleft_entry * S ((S (fom_index_pfp_division_identity_resultproductleft)) * qc) + (fom_value_pfp_division_identity_resultproductleft))) /\ (exists fom_gap_pfp_division_identity_resultproductleft_value_bound. fom_gap_pfp_division_identity_resultproductleft_value_bound + S (fom_value_pfp_division_identity_resultproductleft) = p))) /\ (((forall fom_index_pfp_division_identity_resultproductright. (exists fom_gap_pfp_division_identity_resultproductright_index_bound. fom_gap_pfp_division_identity_resultproductright_index_bound + S (fom_index_pfp_division_identity_resultproductright) = S (d)) -> exists fom_value_pfp_division_identity_resultproductright. ((((exists fom_beta_height_pfp_division_identity_resultproductright_entry. fom_beta_height_pfp_division_identity_resultproductright_entry + S (fom_value_pfp_division_identity_resultproductright) = S ((S (fom_index_pfp_division_identity_resultproductright)) * bc)) /\ exists fom_beta_quotient_pfp_division_identity_resultproductright_entry. bb = fom_beta_quotient_pfp_division_identity_resultproductright_entry * S ((S (fom_index_pfp_division_identity_resultproductright)) * bc) + (fom_value_pfp_division_identity_resultproductright))) /\ (exists fom_gap_pfp_division_identity_resultproductright_value_bound. fom_gap_pfp_division_identity_resultproductright_value_bound + S (fom_value_pfp_division_identity_resultproductright) = p))) /\ (((((((q)=0 \/ (S (d))=0) /\ (((L)=0)))) \/ (((~((q)=0)) /\ (((~((S (d))=0)) /\ (((q)+(S (d))=S (L)))))))) /\ ((forall pfc_index_division_identity_resultproductcoefficients. (exists pfa_gap_division_identity_resultproductcoefficientsbound. pfa_gap_division_identity_resultproductcoefficientsbound + S (pfc_index_division_identity_resultproductcoefficients) = (L)) -> exists pfc_value_division_identity_resultproductcoefficients. ((((exists ff_h_pfp_division_identity_resultproductcoefficientsentry. ff_h_pfp_division_identity_resultproductcoefficientsentry + S (pfc_value_division_identity_resultproductcoefficients) = S ((S (pfc_index_division_identity_resultproductcoefficients)) * pfd_identity_pc_division_identity_result)) /\ exists ff_q_pfp_division_identity_resultproductcoefficientsentry. pfd_identity_pb_division_identity_result = ff_q_pfp_division_identity_resultproductcoefficientsentry * S ((S (pfc_index_division_identity_resultproductcoefficients)) * pfd_identity_pc_division_identity_result) + (pfc_value_division_identity_resultproductcoefficients))) /\ ((exists pfc_terms_code_division_identity_resultproductcoefficientscoefficient pfc_terms_scale_division_identity_resultproductcoefficientscoefficient pfc_natural_sum_division_identity_resultproductcoefficientscoefficient. ((forall pfc_index_division_identity_resultproductcoefficientscoefficientdiagonal. (exists pfa_gap_division_identity_resultproductcoefficientscoefficientdiagonalbound. pfa_gap_division_identity_resultproductcoefficientscoefficientdiagonalbound + S (pfc_index_division_identity_resultproductcoefficientscoefficientdiagonal) = (S (pfc_index_division_identity_resultproductcoefficients))) -> exists pfc_value_division_identity_resultproductcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_division_identity_resultproductcoefficientscoefficientdiagonalentry. ff_h_pfp_division_identity_resultproductcoefficientscoefficientdiagonalentry + S (pfc_value_division_identity_resultproductcoefficientscoefficientdiagonal) = S ((S (pfc_index_division_identity_resultproductcoefficientscoefficientdiagonal)) * pfc_terms_scale_division_identity_resultproductcoefficientscoefficient)) /\ exists ff_q_pfp_division_identity_resultproductcoefficientscoefficientdiagonalentry. pfc_terms_code_division_identity_resultproductcoefficientscoefficient = ff_q_pfp_division_identity_resultproductcoefficientscoefficientdiagonalentry * S ((S (pfc_index_division_identity_resultproductcoefficientscoefficientdiagonal)) * pfc_terms_scale_division_identity_resultproductcoefficientscoefficient) + (pfc_value_division_identity_resultproductcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_division_identity_resultproductcoefficientscoefficientdiagonalterm pfc_left_division_identity_resultproductcoefficientscoefficientdiagonalterm pfc_right_division_identity_resultproductcoefficientscoefficientdiagonalterm. (((pfc_index_division_identity_resultproductcoefficientscoefficientdiagonal)+pfc_complement_division_identity_resultproductcoefficientscoefficientdiagonalterm=(pfc_index_division_identity_resultproductcoefficients)) /\ ((((((exists pfa_gap_division_identity_resultproductcoefficientscoefficientdiagonaltermleftinside. pfa_gap_division_identity_resultproductcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_division_identity_resultproductcoefficientscoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_identity_resultproductcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_division_identity_resultproductcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_division_identity_resultproductcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_division_identity_resultproductcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_identity_resultproductcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_identity_resultproductcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_division_identity_resultproductcoefficientscoefficientdiagonal)) * qc) + (pfc_left_division_identity_resultproductcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_identity_resultproductcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_division_identity_resultproductcoefficientscoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_identity_resultproductcoefficientscoefficientdiagonal)) /\ (((pfc_left_division_identity_resultproductcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_identity_resultproductcoefficientscoefficientdiagonaltermrightinside. pfa_gap_division_identity_resultproductcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_division_identity_resultproductcoefficientscoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_identity_resultproductcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_division_identity_resultproductcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_division_identity_resultproductcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_division_identity_resultproductcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_identity_resultproductcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_identity_resultproductcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_identity_resultproductcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_division_identity_resultproductcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_identity_resultproductcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_division_identity_resultproductcoefficientscoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_identity_resultproductcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_division_identity_resultproductcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_identity_resultproductcoefficientscoefficientdiagonal)=pfc_left_division_identity_resultproductcoefficientscoefficientdiagonalterm*pfc_right_division_identity_resultproductcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_identity_resultproductcoefficientscoefficientsum fs_v_pfc_division_identity_resultproductcoefficientscoefficientsum. ((((exists fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_start. fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_identity_resultproductcoefficientscoefficientsum)) /\ exists fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_start. fs_u_pfc_division_identity_resultproductcoefficientscoefficientsum = fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_identity_resultproductcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_terminal. fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_division_identity_resultproductcoefficientscoefficient) = S ((S (S (pfc_index_division_identity_resultproductcoefficients))) * fs_v_pfc_division_identity_resultproductcoefficientscoefficientsum)) /\ exists fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_terminal. fs_u_pfc_division_identity_resultproductcoefficientscoefficientsum = fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_division_identity_resultproductcoefficients))) * fs_v_pfc_division_identity_resultproductcoefficientscoefficientsum) + (pfc_natural_sum_division_identity_resultproductcoefficientscoefficient))) /\ forall fs_i_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps = S (pfc_index_division_identity_resultproductcoefficients)) -> exists fs_a_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps fs_r_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps fs_s_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_division_identity_resultproductcoefficientscoefficient)) /\ exists fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_division_identity_resultproductcoefficientscoefficient = fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_division_identity_resultproductcoefficientscoefficient) + (fs_a_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps)) * fs_v_pfc_division_identity_resultproductcoefficientscoefficientsum)) /\ exists fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_division_identity_resultproductcoefficientscoefficientsum = fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps)) * fs_v_pfc_division_identity_resultproductcoefficientscoefficientsum) + (fs_r_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps)) * fs_v_pfc_division_identity_resultproductcoefficientscoefficientsum)) /\ exists fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_division_identity_resultproductcoefficientscoefficientsum = fs_q_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps)) * fs_v_pfc_division_identity_resultproductcoefficientscoefficientsum) + (fs_s_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps = fs_r_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps + fs_a_pfc_division_identity_resultproductcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_identity_resultproductcoefficientscoefficientresiduebound. pfa_gap_division_identity_resultproductcoefficientscoefficientresiduebound + S (pfc_value_division_identity_resultproductcoefficients) = (p)) /\ ((exists pfa_offset_left_division_identity_resultproductcoefficientscoefficientresiduecongruence pfa_offset_right_division_identity_resultproductcoefficientscoefficientresiduecongruence. (pfc_natural_sum_division_identity_resultproductcoefficientscoefficient) + (p) * pfa_offset_left_division_identity_resultproductcoefficientscoefficientresiduecongruence = (pfc_value_division_identity_resultproductcoefficients) + (p) * pfa_offset_right_division_identity_resultproductcoefficientscoefficientresiduecongruence))))))))))))))))))))))) /\ (((forall pfp_index_division_identity_resultaddition. (exists pfa_gap_division_identity_resultadditionindex. pfa_gap_division_identity_resultadditionindex + S (pfp_index_division_identity_resultaddition) = (L)) -> exists pfp_left_division_identity_resultaddition pfp_right_division_identity_resultaddition pfp_value_division_identity_resultaddition. ((((exists ff_h_pfp_division_identity_resultadditionleft. ff_h_pfp_division_identity_resultadditionleft + S (pfp_left_division_identity_resultaddition) = S ((S (pfp_index_division_identity_resultaddition)) * pfd_identity_pc_division_identity_result)) /\ exists ff_q_pfp_division_identity_resultadditionleft. pfd_identity_pb_division_identity_result = ff_q_pfp_division_identity_resultadditionleft * S ((S (pfp_index_division_identity_resultaddition)) * pfd_identity_pc_division_identity_result) + (pfp_left_division_identity_resultaddition))) /\ (((((exists ff_h_pfp_division_identity_resultadditionright. ff_h_pfp_division_identity_resultadditionright + S (pfp_right_division_identity_resultaddition) = S ((S (pfp_index_division_identity_resultaddition)) * pfd_identity_uc_division_identity_result)) /\ exists ff_q_pfp_division_identity_resultadditionright. pfd_identity_ub_division_identity_result = ff_q_pfp_division_identity_resultadditionright * S ((S (pfp_index_division_identity_resultaddition)) * pfd_identity_uc_division_identity_result) + (pfp_right_division_identity_resultaddition))) /\ (((((exists ff_h_pfp_division_identity_resultadditiontarget. ff_h_pfp_division_identity_resultadditiontarget + S (pfp_value_division_identity_resultaddition) = S ((S (pfp_index_division_identity_resultaddition)) * ac)) /\ exists ff_q_pfp_division_identity_resultadditiontarget. ab = ff_q_pfp_division_identity_resultadditiontarget * S ((S (pfp_index_division_identity_resultaddition)) * ac) + (pfp_value_division_identity_resultaddition))) /\ ((((exists pfa_gap_division_identity_resultadditionoperationleft. pfa_gap_division_identity_resultadditionoperationleft + S (pfp_left_division_identity_resultaddition) = (p)) /\ (((exists pfa_gap_division_identity_resultadditionoperationright. pfa_gap_division_identity_resultadditionoperationright + S (pfp_right_division_identity_resultaddition) = (p)) /\ ((((exists pfa_gap_division_identity_resultadditionoperationresultbound. pfa_gap_division_identity_resultadditionoperationresultbound + S (pfp_value_division_identity_resultaddition) = (p)) /\ ((exists pfa_offset_left_division_identity_resultadditionoperationresultcongruence pfa_offset_right_division_identity_resultadditionoperationresultcongruence. ((pfp_left_division_identity_resultaddition) + (pfp_right_division_identity_resultaddition)) + (p) * pfa_offset_left_division_identity_resultadditionoperationresultcongruence = (pfp_value_division_identity_resultaddition) + (p) * pfa_offset_right_division_identity_resultadditionoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_identity_t_division_identity_result)+(R)) /\ (((forall fom_index_pfp_division_identity_resultremainderinput. (exists fom_gap_pfp_division_identity_resultremainderinput_index_bound. fom_gap_pfp_division_identity_resultremainderinput_index_bound + S (fom_index_pfp_division_identity_resultremainderinput) = L) -> exists fom_value_pfp_division_identity_resultremainderinput. ((((exists fom_beta_height_pfp_division_identity_resultremainderinput_entry. fom_beta_height_pfp_division_identity_resultremainderinput_entry + S (fom_value_pfp_division_identity_resultremainderinput) = S ((S (fom_index_pfp_division_identity_resultremainderinput)) * pfd_identity_uc_division_identity_result)) /\ exists fom_beta_quotient_pfp_division_identity_resultremainderinput_entry. pfd_identity_ub_division_identity_result = fom_beta_quotient_pfp_division_identity_resultremainderinput_entry * S ((S (fom_index_pfp_division_identity_resultremainderinput)) * pfd_identity_uc_division_identity_result) + (fom_value_pfp_division_identity_resultremainderinput))) /\ (exists fom_gap_pfp_division_identity_resultremainderinput_value_bound. fom_gap_pfp_division_identity_resultremainderinput_value_bound + S (fom_value_pfp_division_identity_resultremainderinput) = p))) /\ (((forall pfp_repeat_index_division_identity_resultremainderremoved. (exists pfa_gap_division_identity_resultremainderremovedindex. pfa_gap_division_identity_resultremainderremovedindex + S (pfp_repeat_index_division_identity_resultremainderremoved) = (pfd_identity_t_division_identity_result)) -> (((exists ff_h_pfp_division_identity_resultremainderremovedentry. ff_h_pfp_division_identity_resultremainderremovedentry + S (0) = S ((S (pfp_repeat_index_division_identity_resultremainderremoved)) * pfd_identity_uc_division_identity_result)) /\ exists ff_q_pfp_division_identity_resultremainderremovedentry. pfd_identity_ub_division_identity_result = ff_q_pfp_division_identity_resultremainderremovedentry * S ((S (pfp_repeat_index_division_identity_resultremainderremoved)) * pfd_identity_uc_division_identity_result) + (0)))) /\ (((forall pftrim_index_division_identity_resultremaindersuffix pftrim_value_division_identity_resultremaindersuffix. (exists pfa_gap_division_identity_resultremaindersuffixbound. pfa_gap_division_identity_resultremaindersuffixbound + S (pftrim_index_division_identity_resultremaindersuffix) = (R)) -> (((exists ff_h_pfp_division_identity_resultremaindersuffixsource. ff_h_pfp_division_identity_resultremaindersuffixsource + S (pftrim_value_division_identity_resultremaindersuffix) = S ((S ((pfd_identity_t_division_identity_result)+pftrim_index_division_identity_resultremaindersuffix)) * pfd_identity_uc_division_identity_result)) /\ exists ff_q_pfp_division_identity_resultremaindersuffixsource. pfd_identity_ub_division_identity_result = ff_q_pfp_division_identity_resultremaindersuffixsource * S ((S ((pfd_identity_t_division_identity_result)+pftrim_index_division_identity_resultremaindersuffix)) * pfd_identity_uc_division_identity_result) + (pftrim_value_division_identity_resultremaindersuffix))) -> (((exists ff_h_pfp_division_identity_resultremaindersuffixoutput. ff_h_pfp_division_identity_resultremaindersuffixoutput + S (pftrim_value_division_identity_resultremaindersuffix) = S ((S (pftrim_index_division_identity_resultremaindersuffix)) * rc)) /\ exists ff_q_pfp_division_identity_resultremaindersuffixoutput. rb = ff_q_pfp_division_identity_resultremaindersuffixoutput * S ((S (pftrim_index_division_identity_resultremaindersuffix)) * rc) + (pftrim_value_division_identity_resultremaindersuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_identity_resultremaindernormal. ((((exists ff_h_pfp_division_identity_resultremaindernormalentry. ff_h_pfp_division_identity_resultremaindernormalentry + S (pftrim_leading_division_identity_resultremaindernormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_identity_resultremaindernormalentry. rb = ff_q_pfp_division_identity_resultremaindernormalentry * S ((S (0)) * rc) + (pftrim_leading_division_identity_resultremaindernormal))) /\ ((~(pftrim_leading_division_identity_resultremaindernormal=0))))))))))))))))))))