PX0039

prime_field_polynomial_division_execution_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Construct general quotient and normalized remainder codes from any canonical input and actual nonzero divisor, without assuming any output identity or degree bound.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc d. (~((p) = 1) /\ forall pfa_factor_left_division_total_prime pfa_factor_right_division_total_prime. (p) = pfa_factor_left_division_total_prime * pfa_factor_right_division_total_prime -> pfa_factor_left_division_total_prime = 1 \/ pfa_factor_right_division_total_prime = 1) -> (forall fom_index_pfp_division_total_input. (exists fom_gap_pfp_division_total_input_index_bound. fom_gap_pfp_division_total_input_index_bound + S (fom_index_pfp_division_total_input) = L) -> exists fom_value_pfp_division_total_input. ((((exists fom_beta_height_pfp_division_total_input_entry. fom_beta_height_pfp_division_total_input_entry + S (fom_value_pfp_division_total_input) = S ((S (fom_index_pfp_division_total_input)) * ac)) /\ exists fom_beta_quotient_pfp_division_total_input_entry. ab = fom_beta_quotient_pfp_division_total_input_entry * S ((S (fom_index_pfp_division_total_input)) * ac) + (fom_value_pfp_division_total_input))) /\ (exists fom_gap_pfp_division_total_input_value_bound. fom_gap_pfp_division_total_input_value_bound + S (fom_value_pfp_division_total_input) = p))) -> ((((S d)=S (d)) /\ (((forall fom_index_pfp_division_total_divisorcoefficients. (exists fom_gap_pfp_division_total_divisorcoefficients_index_bound. fom_gap_pfp_division_total_divisorcoefficients_index_bound + S (fom_index_pfp_division_total_divisorcoefficients) = S d) -> exists fom_value_pfp_division_total_divisorcoefficients. ((((exists fom_beta_height_pfp_division_total_divisorcoefficients_entry. fom_beta_height_pfp_division_total_divisorcoefficients_entry + S (fom_value_pfp_division_total_divisorcoefficients) = S ((S (fom_index_pfp_division_total_divisorcoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_division_total_divisorcoefficients_entry. bb = fom_beta_quotient_pfp_division_total_divisorcoefficients_entry * S ((S (fom_index_pfp_division_total_divisorcoefficients)) * bc) + (fom_value_pfp_division_total_divisorcoefficients))) /\ (exists fom_gap_pfp_division_total_divisorcoefficients_value_bound. fom_gap_pfp_division_total_divisorcoefficients_value_bound + S (fom_value_pfp_division_total_divisorcoefficients) = p))) /\ ((exists pfd_leading_division_total_divisor. ((((exists ff_h_pfp_division_total_divisorentry. ff_h_pfp_division_total_divisorentry + S (pfd_leading_division_total_divisor) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_total_divisorentry. bb = ff_q_pfp_division_total_divisorentry * S ((S (0)) * bc) + (pfd_leading_division_total_divisor))) /\ ((~(pfd_leading_division_total_divisor=0)))))))))) -> exists qb qc q rb rc R. (((forall fom_index_pfp_division_total_resultinput. (exists fom_gap_pfp_division_total_resultinput_index_bound. fom_gap_pfp_division_total_resultinput_index_bound + S (fom_index_pfp_division_total_resultinput) = L) -> exists fom_value_pfp_division_total_resultinput. ((((exists fom_beta_height_pfp_division_total_resultinput_entry. fom_beta_height_pfp_division_total_resultinput_entry + S (fom_value_pfp_division_total_resultinput) = S ((S (fom_index_pfp_division_total_resultinput)) * ac)) /\ exists fom_beta_quotient_pfp_division_total_resultinput_entry. ab = fom_beta_quotient_pfp_division_total_resultinput_entry * S ((S (fom_index_pfp_division_total_resultinput)) * ac) + (fom_value_pfp_division_total_resultinput))) /\ (exists fom_gap_pfp_division_total_resultinput_value_bound. fom_gap_pfp_division_total_resultinput_value_bound + S (fom_value_pfp_division_total_resultinput) = p))) /\ (((forall fom_index_pfp_division_total_resultdivisor. (exists fom_gap_pfp_division_total_resultdivisor_index_bound. fom_gap_pfp_division_total_resultdivisor_index_bound + S (fom_index_pfp_division_total_resultdivisor) = S (d)) -> exists fom_value_pfp_division_total_resultdivisor. ((((exists fom_beta_height_pfp_division_total_resultdivisor_entry. fom_beta_height_pfp_division_total_resultdivisor_entry + S (fom_value_pfp_division_total_resultdivisor) = S ((S (fom_index_pfp_division_total_resultdivisor)) * bc)) /\ exists fom_beta_quotient_pfp_division_total_resultdivisor_entry. bb = fom_beta_quotient_pfp_division_total_resultdivisor_entry * S ((S (fom_index_pfp_division_total_resultdivisor)) * bc) + (fom_value_pfp_division_total_resultdivisor))) /\ (exists fom_gap_pfp_division_total_resultdivisor_value_bound. fom_gap_pfp_division_total_resultdivisor_value_bound + S (fom_value_pfp_division_total_resultdivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_division_total_resultlengthshort. pfc_gap_division_total_resultlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_division_total_result pfd_inverse_division_total_result pfd_product_code_division_total_result pfd_product_scale_division_total_result pfd_residual_code_division_total_result pfd_residual_scale_division_total_result pfd_cut_division_total_result. ((((exists ff_h_pfp_division_total_resulthead. ff_h_pfp_division_total_resulthead + S (pfd_head_division_total_result) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_total_resulthead. bb = ff_q_pfp_division_total_resulthead * S ((S (0)) * bc) + (pfd_head_division_total_result))) /\ (((((~((pfd_head_division_total_result) = 0)) /\ ((((exists pfa_gap_division_total_resultinversemultiplicationleft. pfa_gap_division_total_resultinversemultiplicationleft + S (pfd_head_division_total_result) = (p)) /\ (((exists pfa_gap_division_total_resultinversemultiplicationright. pfa_gap_division_total_resultinversemultiplicationright + S (pfd_inverse_division_total_result) = (p)) /\ ((((exists pfa_gap_division_total_resultinversemultiplicationresultbound. pfa_gap_division_total_resultinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_total_resultinversemultiplicationresultcongruence pfa_offset_right_division_total_resultinversemultiplicationresultcongruence. ((pfd_head_division_total_result) * (pfd_inverse_division_total_result)) + (p) * pfa_offset_left_division_total_resultinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_total_resultinversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_division_total_resultquotient. (exists pfa_gap_division_total_resultquotientbound. pfa_gap_division_total_resultquotientbound + S (pfd_index_division_total_resultquotient) = (q)) -> exists pfd_value_division_total_resultquotient. ((((exists ff_h_pfp_division_total_resultquotiententry. ff_h_pfp_division_total_resultquotiententry + S (pfd_value_division_total_resultquotient) = S ((S (pfd_index_division_total_resultquotient)) * qc)) /\ exists ff_q_pfp_division_total_resultquotiententry. qb = ff_q_pfp_division_total_resultquotiententry * S ((S (pfd_index_division_total_resultquotient)) * qc) + (pfd_value_division_total_resultquotient))) /\ ((exists pfd_input_division_total_resultquotientstep pfd_previous_division_total_resultquotientstep pfd_difference_division_total_resultquotientstep. ((((exists ff_h_pfp_division_total_resultquotientstepinput. ff_h_pfp_division_total_resultquotientstepinput + S (pfd_input_division_total_resultquotientstep) = S ((S (pfd_index_division_total_resultquotient)) * ac)) /\ exists ff_q_pfp_division_total_resultquotientstepinput. ab = ff_q_pfp_division_total_resultquotientstepinput * S ((S (pfd_index_division_total_resultquotient)) * ac) + (pfd_input_division_total_resultquotientstep))) /\ (((exists pfc_terms_code_division_total_resultquotientstepprevious pfc_terms_scale_division_total_resultquotientstepprevious pfc_natural_sum_division_total_resultquotientstepprevious. ((forall pfc_index_division_total_resultquotientsteppreviousdiagonal. (exists pfa_gap_division_total_resultquotientsteppreviousdiagonalbound. pfa_gap_division_total_resultquotientsteppreviousdiagonalbound + S (pfc_index_division_total_resultquotientsteppreviousdiagonal) = (S (pfd_index_division_total_resultquotient))) -> exists pfc_value_division_total_resultquotientsteppreviousdiagonal. ((((exists ff_h_pfp_division_total_resultquotientsteppreviousdiagonalentry. ff_h_pfp_division_total_resultquotientsteppreviousdiagonalentry + S (pfc_value_division_total_resultquotientsteppreviousdiagonal) = S ((S (pfc_index_division_total_resultquotientsteppreviousdiagonal)) * pfc_terms_scale_division_total_resultquotientstepprevious)) /\ exists ff_q_pfp_division_total_resultquotientsteppreviousdiagonalentry. pfc_terms_code_division_total_resultquotientstepprevious = ff_q_pfp_division_total_resultquotientsteppreviousdiagonalentry * S ((S (pfc_index_division_total_resultquotientsteppreviousdiagonal)) * pfc_terms_scale_division_total_resultquotientstepprevious) + (pfc_value_division_total_resultquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_division_total_resultquotientsteppreviousdiagonalterm pfc_left_division_total_resultquotientsteppreviousdiagonalterm pfc_right_division_total_resultquotientsteppreviousdiagonalterm. (((pfc_index_division_total_resultquotientsteppreviousdiagonal)+pfc_complement_division_total_resultquotientsteppreviousdiagonalterm=(pfd_index_division_total_resultquotient)) /\ ((((((exists pfa_gap_division_total_resultquotientsteppreviousdiagonaltermleftinside. pfa_gap_division_total_resultquotientsteppreviousdiagonaltermleftinside + S (pfc_index_division_total_resultquotientsteppreviousdiagonal) = (pfd_index_division_total_resultquotient)) /\ ((((exists ff_h_pfp_division_total_resultquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_division_total_resultquotientsteppreviousdiagonaltermleftentry + S (pfc_left_division_total_resultquotientsteppreviousdiagonalterm) = S ((S (pfc_index_division_total_resultquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_total_resultquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_total_resultquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_total_resultquotientsteppreviousdiagonal)) * qc) + (pfc_left_division_total_resultquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_total_resultquotientsteppreviousdiagonaltermleftoutside. pfc_gap_division_total_resultquotientsteppreviousdiagonaltermleftoutside+(pfd_index_division_total_resultquotient)=(pfc_index_division_total_resultquotientsteppreviousdiagonal)) /\ (((pfc_left_division_total_resultquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_total_resultquotientsteppreviousdiagonaltermrightinside. pfa_gap_division_total_resultquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_division_total_resultquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_total_resultquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_division_total_resultquotientsteppreviousdiagonaltermrightentry + S (pfc_right_division_total_resultquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_division_total_resultquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_total_resultquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_total_resultquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_total_resultquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_division_total_resultquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_total_resultquotientsteppreviousdiagonaltermrightoutside. pfc_gap_division_total_resultquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_division_total_resultquotientsteppreviousdiagonalterm)) /\ (((pfc_right_division_total_resultquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_total_resultquotientsteppreviousdiagonal)=pfc_left_division_total_resultquotientsteppreviousdiagonalterm*pfc_right_division_total_resultquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_total_resultquotientstepprevioussum fs_v_pfc_division_total_resultquotientstepprevioussum. ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_start. fs_h_pfc_division_total_resultquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_total_resultquotientstepprevioussum)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_start. fs_u_pfc_division_total_resultquotientstepprevioussum = fs_q_pfc_division_total_resultquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_total_resultquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_terminal. fs_h_pfc_division_total_resultquotientstepprevioussum_body_terminal + S (pfc_natural_sum_division_total_resultquotientstepprevious) = S ((S (S (pfd_index_division_total_resultquotient))) * fs_v_pfc_division_total_resultquotientstepprevioussum)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_terminal. fs_u_pfc_division_total_resultquotientstepprevioussum = fs_q_pfc_division_total_resultquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_division_total_resultquotient))) * fs_v_pfc_division_total_resultquotientstepprevioussum) + (pfc_natural_sum_division_total_resultquotientstepprevious))) /\ forall fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps. (exists fs_lt_pfc_division_total_resultquotientstepprevioussum_body_steps_bound. fs_lt_pfc_division_total_resultquotientstepprevioussum_body_steps_bound + S fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps = S (pfd_index_division_total_resultquotient)) -> exists fs_a_pfc_division_total_resultquotientstepprevioussum_body_steps fs_r_pfc_division_total_resultquotientstepprevioussum_body_steps fs_s_pfc_division_total_resultquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_summand. fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_division_total_resultquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_total_resultquotientstepprevious)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_summand. pfc_terms_code_division_total_resultquotientstepprevious = fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_total_resultquotientstepprevious) + (fs_a_pfc_division_total_resultquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_partial. fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_division_total_resultquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * fs_v_pfc_division_total_resultquotientstepprevioussum)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_partial. fs_u_pfc_division_total_resultquotientstepprevioussum = fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * fs_v_pfc_division_total_resultquotientstepprevioussum) + (fs_r_pfc_division_total_resultquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_successor. fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_division_total_resultquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * fs_v_pfc_division_total_resultquotientstepprevioussum)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_successor. fs_u_pfc_division_total_resultquotientstepprevioussum = fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * fs_v_pfc_division_total_resultquotientstepprevioussum) + (fs_s_pfc_division_total_resultquotientstepprevioussum_body_steps))) /\ fs_s_pfc_division_total_resultquotientstepprevioussum_body_steps = fs_r_pfc_division_total_resultquotientstepprevioussum_body_steps + fs_a_pfc_division_total_resultquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_total_resultquotientsteppreviousresiduebound. pfa_gap_division_total_resultquotientsteppreviousresiduebound + S (pfd_previous_division_total_resultquotientstep) = (p)) /\ ((exists pfa_offset_left_division_total_resultquotientsteppreviousresiduecongruence pfa_offset_right_division_total_resultquotientsteppreviousresiduecongruence. (pfc_natural_sum_division_total_resultquotientstepprevious) + (p) * pfa_offset_left_division_total_resultquotientsteppreviousresiduecongruence = (pfd_previous_division_total_resultquotientstep) + (p) * pfa_offset_right_division_total_resultquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_total_resultquotientstepsubtractleft. pfa_gap_division_total_resultquotientstepsubtractleft + S (pfd_previous_division_total_resultquotientstep) = (p)) /\ (((exists pfa_gap_division_total_resultquotientstepsubtractright. pfa_gap_division_total_resultquotientstepsubtractright + S (pfd_difference_division_total_resultquotientstep) = (p)) /\ ((((exists pfa_gap_division_total_resultquotientstepsubtractresultbound. pfa_gap_division_total_resultquotientstepsubtractresultbound + S (pfd_input_division_total_resultquotientstep) = (p)) /\ ((exists pfa_offset_left_division_total_resultquotientstepsubtractresultcongruence pfa_offset_right_division_total_resultquotientstepsubtractresultcongruence. ((pfd_previous_division_total_resultquotientstep) + (pfd_difference_division_total_resultquotientstep)) + (p) * pfa_offset_left_division_total_resultquotientstepsubtractresultcongruence = (pfd_input_division_total_resultquotientstep) + (p) * pfa_offset_right_division_total_resultquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_total_resultquotientstepmultiplyleft. pfa_gap_division_total_resultquotientstepmultiplyleft + S (pfd_inverse_division_total_result) = (p)) /\ (((exists pfa_gap_division_total_resultquotientstepmultiplyright. pfa_gap_division_total_resultquotientstepmultiplyright + S (pfd_difference_division_total_resultquotientstep) = (p)) /\ ((((exists pfa_gap_division_total_resultquotientstepmultiplyresultbound. pfa_gap_division_total_resultquotientstepmultiplyresultbound + S (pfd_value_division_total_resultquotient) = (p)) /\ ((exists pfa_offset_left_division_total_resultquotientstepmultiplyresultcongruence pfa_offset_right_division_total_resultquotientstepmultiplyresultcongruence. ((pfd_inverse_division_total_result) * (pfd_difference_division_total_resultquotientstep)) + (p) * pfa_offset_left_division_total_resultquotientstepmultiplyresultcongruence = (pfd_value_division_total_resultquotient) + (p) * pfa_offset_right_division_total_resultquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_division_total_resultproduct. (exists pfa_gap_division_total_resultproductbound. pfa_gap_division_total_resultproductbound + S (pfc_index_division_total_resultproduct) = (L)) -> exists pfc_value_division_total_resultproduct. ((((exists ff_h_pfp_division_total_resultproductentry. ff_h_pfp_division_total_resultproductentry + S (pfc_value_division_total_resultproduct) = S ((S (pfc_index_division_total_resultproduct)) * pfd_product_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resultproductentry. pfd_product_code_division_total_result = ff_q_pfp_division_total_resultproductentry * S ((S (pfc_index_division_total_resultproduct)) * pfd_product_scale_division_total_result) + (pfc_value_division_total_resultproduct))) /\ ((exists pfc_terms_code_division_total_resultproductcoefficient pfc_terms_scale_division_total_resultproductcoefficient pfc_natural_sum_division_total_resultproductcoefficient. ((forall pfc_index_division_total_resultproductcoefficientdiagonal. (exists pfa_gap_division_total_resultproductcoefficientdiagonalbound. pfa_gap_division_total_resultproductcoefficientdiagonalbound + S (pfc_index_division_total_resultproductcoefficientdiagonal) = (S (pfc_index_division_total_resultproduct))) -> exists pfc_value_division_total_resultproductcoefficientdiagonal. ((((exists ff_h_pfp_division_total_resultproductcoefficientdiagonalentry. ff_h_pfp_division_total_resultproductcoefficientdiagonalentry + S (pfc_value_division_total_resultproductcoefficientdiagonal) = S ((S (pfc_index_division_total_resultproductcoefficientdiagonal)) * pfc_terms_scale_division_total_resultproductcoefficient)) /\ exists ff_q_pfp_division_total_resultproductcoefficientdiagonalentry. pfc_terms_code_division_total_resultproductcoefficient = ff_q_pfp_division_total_resultproductcoefficientdiagonalentry * S ((S (pfc_index_division_total_resultproductcoefficientdiagonal)) * pfc_terms_scale_division_total_resultproductcoefficient) + (pfc_value_division_total_resultproductcoefficientdiagonal))) /\ ((exists pfc_complement_division_total_resultproductcoefficientdiagonalterm pfc_left_division_total_resultproductcoefficientdiagonalterm pfc_right_division_total_resultproductcoefficientdiagonalterm. (((pfc_index_division_total_resultproductcoefficientdiagonal)+pfc_complement_division_total_resultproductcoefficientdiagonalterm=(pfc_index_division_total_resultproduct)) /\ ((((((exists pfa_gap_division_total_resultproductcoefficientdiagonaltermleftinside. pfa_gap_division_total_resultproductcoefficientdiagonaltermleftinside + S (pfc_index_division_total_resultproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_total_resultproductcoefficientdiagonaltermleftentry. ff_h_pfp_division_total_resultproductcoefficientdiagonaltermleftentry + S (pfc_left_division_total_resultproductcoefficientdiagonalterm) = S ((S (pfc_index_division_total_resultproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_total_resultproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_total_resultproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_total_resultproductcoefficientdiagonal)) * qc) + (pfc_left_division_total_resultproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_total_resultproductcoefficientdiagonaltermleftoutside. pfc_gap_division_total_resultproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_total_resultproductcoefficientdiagonal)) /\ (((pfc_left_division_total_resultproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_total_resultproductcoefficientdiagonaltermrightinside. pfa_gap_division_total_resultproductcoefficientdiagonaltermrightinside + S (pfc_complement_division_total_resultproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_total_resultproductcoefficientdiagonaltermrightentry. ff_h_pfp_division_total_resultproductcoefficientdiagonaltermrightentry + S (pfc_right_division_total_resultproductcoefficientdiagonalterm) = S ((S (pfc_complement_division_total_resultproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_total_resultproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_total_resultproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_total_resultproductcoefficientdiagonalterm)) * bc) + (pfc_right_division_total_resultproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_total_resultproductcoefficientdiagonaltermrightoutside. pfc_gap_division_total_resultproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_total_resultproductcoefficientdiagonalterm)) /\ (((pfc_right_division_total_resultproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_total_resultproductcoefficientdiagonal)=pfc_left_division_total_resultproductcoefficientdiagonalterm*pfc_right_division_total_resultproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_total_resultproductcoefficientsum fs_v_pfc_division_total_resultproductcoefficientsum. ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_start. fs_h_pfc_division_total_resultproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_total_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_start. fs_u_pfc_division_total_resultproductcoefficientsum = fs_q_pfc_division_total_resultproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_total_resultproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_terminal. fs_h_pfc_division_total_resultproductcoefficientsum_body_terminal + S (pfc_natural_sum_division_total_resultproductcoefficient) = S ((S (S (pfc_index_division_total_resultproduct))) * fs_v_pfc_division_total_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_terminal. fs_u_pfc_division_total_resultproductcoefficientsum = fs_q_pfc_division_total_resultproductcoefficientsum_body_terminal * S ((S (S (pfc_index_division_total_resultproduct))) * fs_v_pfc_division_total_resultproductcoefficientsum) + (pfc_natural_sum_division_total_resultproductcoefficient))) /\ forall fs_i_pfc_division_total_resultproductcoefficientsum_body_steps. (exists fs_lt_pfc_division_total_resultproductcoefficientsum_body_steps_bound. fs_lt_pfc_division_total_resultproductcoefficientsum_body_steps_bound + S fs_i_pfc_division_total_resultproductcoefficientsum_body_steps = S (pfc_index_division_total_resultproduct)) -> exists fs_a_pfc_division_total_resultproductcoefficientsum_body_steps fs_r_pfc_division_total_resultproductcoefficientsum_body_steps fs_s_pfc_division_total_resultproductcoefficientsum_body_steps. ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_summand. fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_summand + S (fs_a_pfc_division_total_resultproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * pfc_terms_scale_division_total_resultproductcoefficient)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_summand. pfc_terms_code_division_total_resultproductcoefficient = fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * pfc_terms_scale_division_total_resultproductcoefficient) + (fs_a_pfc_division_total_resultproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_partial. fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_partial + S (fs_r_pfc_division_total_resultproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_partial. fs_u_pfc_division_total_resultproductcoefficientsum = fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_resultproductcoefficientsum) + (fs_r_pfc_division_total_resultproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_successor. fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_successor + S (fs_s_pfc_division_total_resultproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_successor. fs_u_pfc_division_total_resultproductcoefficientsum = fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_resultproductcoefficientsum) + (fs_s_pfc_division_total_resultproductcoefficientsum_body_steps))) /\ fs_s_pfc_division_total_resultproductcoefficientsum_body_steps = fs_r_pfc_division_total_resultproductcoefficientsum_body_steps + fs_a_pfc_division_total_resultproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_total_resultproductcoefficientresiduebound. pfa_gap_division_total_resultproductcoefficientresiduebound + S (pfc_value_division_total_resultproduct) = (p)) /\ ((exists pfa_offset_left_division_total_resultproductcoefficientresiduecongruence pfa_offset_right_division_total_resultproductcoefficientresiduecongruence. (pfc_natural_sum_division_total_resultproductcoefficient) + (p) * pfa_offset_left_division_total_resultproductcoefficientresiduecongruence = (pfc_value_division_total_resultproduct) + (p) * pfa_offset_right_division_total_resultproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_division_total_resultdifference. (exists pfa_gap_division_total_resultdifferenceindex. pfa_gap_division_total_resultdifferenceindex + S (pfs_index_division_total_resultdifference) = (L)) -> exists pfs_left_division_total_resultdifference pfs_right_division_total_resultdifference pfs_result_division_total_resultdifference. ((((exists ff_h_pfp_division_total_resultdifferenceleft. ff_h_pfp_division_total_resultdifferenceleft + S (pfs_left_division_total_resultdifference) = S ((S (pfs_index_division_total_resultdifference)) * ac)) /\ exists ff_q_pfp_division_total_resultdifferenceleft. ab = ff_q_pfp_division_total_resultdifferenceleft * S ((S (pfs_index_division_total_resultdifference)) * ac) + (pfs_left_division_total_resultdifference))) /\ (((((exists ff_h_pfp_division_total_resultdifferenceright. ff_h_pfp_division_total_resultdifferenceright + S (pfs_right_division_total_resultdifference) = S ((S (pfs_index_division_total_resultdifference)) * pfd_product_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resultdifferenceright. pfd_product_code_division_total_result = ff_q_pfp_division_total_resultdifferenceright * S ((S (pfs_index_division_total_resultdifference)) * pfd_product_scale_division_total_result) + (pfs_right_division_total_resultdifference))) /\ (((((exists ff_h_pfp_division_total_resultdifferenceresult. ff_h_pfp_division_total_resultdifferenceresult + S (pfs_result_division_total_resultdifference) = S ((S (pfs_index_division_total_resultdifference)) * pfd_residual_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resultdifferenceresult. pfd_residual_code_division_total_result = ff_q_pfp_division_total_resultdifferenceresult * S ((S (pfs_index_division_total_resultdifference)) * pfd_residual_scale_division_total_result) + (pfs_result_division_total_resultdifference))) /\ ((((exists pfa_gap_division_total_resultdifferenceoperationleft. pfa_gap_division_total_resultdifferenceoperationleft + S (pfs_right_division_total_resultdifference) = (p)) /\ (((exists pfa_gap_division_total_resultdifferenceoperationright. pfa_gap_division_total_resultdifferenceoperationright + S (pfs_result_division_total_resultdifference) = (p)) /\ ((((exists pfa_gap_division_total_resultdifferenceoperationresultbound. pfa_gap_division_total_resultdifferenceoperationresultbound + S (pfs_left_division_total_resultdifference) = (p)) /\ ((exists pfa_offset_left_division_total_resultdifferenceoperationresultcongruence pfa_offset_right_division_total_resultdifferenceoperationresultcongruence. ((pfs_right_division_total_resultdifference) + (pfs_result_division_total_resultdifference)) + (p) * pfa_offset_left_division_total_resultdifferenceoperationresultcongruence = (pfs_left_division_total_resultdifference) + (p) * pfa_offset_right_division_total_resultdifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_division_total_result)+(R)) /\ (((forall fom_index_pfp_division_total_resulttriminput. (exists fom_gap_pfp_division_total_resulttriminput_index_bound. fom_gap_pfp_division_total_resulttriminput_index_bound + S (fom_index_pfp_division_total_resulttriminput) = L) -> exists fom_value_pfp_division_total_resulttriminput. ((((exists fom_beta_height_pfp_division_total_resulttriminput_entry. fom_beta_height_pfp_division_total_resulttriminput_entry + S (fom_value_pfp_division_total_resulttriminput) = S ((S (fom_index_pfp_division_total_resulttriminput)) * pfd_residual_scale_division_total_result)) /\ exists fom_beta_quotient_pfp_division_total_resulttriminput_entry. pfd_residual_code_division_total_result = fom_beta_quotient_pfp_division_total_resulttriminput_entry * S ((S (fom_index_pfp_division_total_resulttriminput)) * pfd_residual_scale_division_total_result) + (fom_value_pfp_division_total_resulttriminput))) /\ (exists fom_gap_pfp_division_total_resulttriminput_value_bound. fom_gap_pfp_division_total_resulttriminput_value_bound + S (fom_value_pfp_division_total_resulttriminput) = p))) /\ (((forall pfp_repeat_index_division_total_resulttrimremoved. (exists pfa_gap_division_total_resulttrimremovedindex. pfa_gap_division_total_resulttrimremovedindex + S (pfp_repeat_index_division_total_resulttrimremoved) = (pfd_cut_division_total_result)) -> (((exists ff_h_pfp_division_total_resulttrimremovedentry. ff_h_pfp_division_total_resulttrimremovedentry + S (0) = S ((S (pfp_repeat_index_division_total_resulttrimremoved)) * pfd_residual_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resulttrimremovedentry. pfd_residual_code_division_total_result = ff_q_pfp_division_total_resulttrimremovedentry * S ((S (pfp_repeat_index_division_total_resulttrimremoved)) * pfd_residual_scale_division_total_result) + (0)))) /\ (((forall pftrim_index_division_total_resulttrimsuffix pftrim_value_division_total_resulttrimsuffix. (exists pfa_gap_division_total_resulttrimsuffixbound. pfa_gap_division_total_resulttrimsuffixbound + S (pftrim_index_division_total_resulttrimsuffix) = (R)) -> (((exists ff_h_pfp_division_total_resulttrimsuffixsource. ff_h_pfp_division_total_resulttrimsuffixsource + S (pftrim_value_division_total_resulttrimsuffix) = S ((S ((pfd_cut_division_total_result)+pftrim_index_division_total_resulttrimsuffix)) * pfd_residual_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resulttrimsuffixsource. pfd_residual_code_division_total_result = ff_q_pfp_division_total_resulttrimsuffixsource * S ((S ((pfd_cut_division_total_result)+pftrim_index_division_total_resulttrimsuffix)) * pfd_residual_scale_division_total_result) + (pftrim_value_division_total_resulttrimsuffix))) -> (((exists ff_h_pfp_division_total_resulttrimsuffixoutput. ff_h_pfp_division_total_resulttrimsuffixoutput + S (pftrim_value_division_total_resulttrimsuffix) = S ((S (pftrim_index_division_total_resulttrimsuffix)) * rc)) /\ exists ff_q_pfp_division_total_resulttrimsuffixoutput. rb = ff_q_pfp_division_total_resulttrimsuffixoutput * S ((S (pftrim_index_division_total_resulttrimsuffix)) * rc) + (pftrim_value_division_total_resulttrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_total_resulttrimnormal. ((((exists ff_h_pfp_division_total_resulttrimnormalentry. ff_h_pfp_division_total_resulttrimnormalentry + S (pftrim_leading_division_total_resulttrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_total_resulttrimnormalentry. rb = ff_q_pfp_division_total_resulttrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_total_resulttrimnormal))) /\ ((~(pftrim_leading_division_total_resulttrimnormal=0)))))))))))))))))))))))))))))))))

Constructive proof overview

Generated structural guide

Construct general quotient and normalized remainder codes from any canonical input and actual nonzero divisor, without assuming any output identity or degree bound.

The unchanged tactic script uses 2 declared prerequisites and contains 86 exact native proof lines.

Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

PX0037 prime_field_polynomial_division_quotient_data_exists PX0038 prime_field_polynomial_division_residual_data_exists

Direct dependents

PX003B prime_field_polynomial_division_exists_with_remainder_bound PX005A prime_field_polynomial_division_execution_exists_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

86 script commands · 26 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
prime field polynomial division quotient data existsprime field polynomial division residual data exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro d
  8. L8
    intro hp
  9. L9
    intro ha
  10. L10
    intro hb
02Establish hquotientL11–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial division quotient data exists.

  1. L11
    have hquotient : ∃ b. ∃ k. ∃ q. ∃ qb. ∃ qc. BetaAt(bb,bc,0,b) ∧ (FpInv(p,b,k) ∧ (PolynomialQuotientLength(L,d,q) ∧ FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,S d,qb,qc,q)))Definitions: FpInvFpPolynomialQuotientPrefixPolynomialQuotientLengthBetaAt
  2. L12
    specialize prime_field_polynomial_division_quotient_data_exists (p)
  3. L13
    specialize prime_field_polynomial_division_quotient_data_exists (ab)
  4. L14
    specialize prime_field_polynomial_division_quotient_data_exists (ac)
  5. L15
    specialize prime_field_polynomial_division_quotient_data_exists (L)
  6. L16
    specialize prime_field_polynomial_division_quotient_data_exists (bb)
  7. L17
    specialize prime_field_polynomial_division_quotient_data_exists (bc)
  8. L18
    specialize prime_field_polynomial_division_quotient_data_exists (d)
  9. L19
    apply prime_field_polynomial_division_quotient_data_exists
  10. L20
    exact hp
03Use earlier factsL21–22

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L21
    exact ha
  2. L22
    exact hb
04Separate the logical casesL23–30

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L23
    cases hquotient
  2. L24
    cases hquotient_witness
  3. L25
    cases hquotient_witness_witness
  4. L26
    cases hquotient_witness_witness_witness
  5. L27
    cases hquotient_witness_witness_witness_witness
  6. L28
    cases hquotient_witness_witness_witness_witness_witness
  7. L29
    cases hquotient_witness_witness_witness_witness_witness_right
  8. L30
    cases hquotient_witness_witness_witness_witness_witness_right_right
05Establish hresidualL31–40

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hresidual : ∃ pb. ∃ pc. ∃ ub. ∃ uc. ∃ t. ∃ rb. ∃ rc. ∃ R. FpConvolutionPrefix(p,x3,x4,x2,bb,bc,S d,pb,pc,L) ∧ (FpCoefficientSubtraction(p,ab,ac,pb,pc,ub,uc,L) ∧ FpPolynomialTrim(p,ub,uc,L,t,rb,rc,R))Definitions: FpConvolutionPrefixFpCoefficientSubtractionFpPolynomialTrim
  2. L32
    specialize prime_field_polynomial_division_residual_data_exists (p)
  3. L33
    specialize prime_field_polynomial_division_residual_data_exists (ab)
  4. L34
    specialize prime_field_polynomial_division_residual_data_exists (ac)
  5. L35
    specialize prime_field_polynomial_division_residual_data_exists (L)
  6. L36
    specialize prime_field_polynomial_division_residual_data_exists (bb)
  7. L37
    specialize prime_field_polynomial_division_residual_data_exists (bc)
  8. L38
    specialize prime_field_polynomial_division_residual_data_exists (d)
  9. L39
    specialize prime_field_polynomial_division_residual_data_exists (x3)
  10. L40
    specialize prime_field_polynomial_division_residual_data_exists (x4)
06Use earlier factsL41–44

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L41
    specialize prime_field_polynomial_division_residual_data_exists (x2)
  2. L42
    apply prime_field_polynomial_division_residual_data_exists
  3. L43
    exact hp
  4. L44
    exact ha
07Separate the logical casesL45–54

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L45
    cases hresidual
  2. L46
    cases hresidual_witness
  3. L47
    cases hresidual_witness_witness
  4. L48
    cases hresidual_witness_witness_witness
  5. L49
    cases hresidual_witness_witness_witness_witness
  6. L50
    cases hresidual_witness_witness_witness_witness_witness
  7. L51
    cases hresidual_witness_witness_witness_witness_witness_witness
  8. L52
    cases hresidual_witness_witness_witness_witness_witness_witness_witness
  9. L53
    cases hresidual_witness_witness_witness_witness_witness_witness_witness_witness
  10. L54
    cases hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right
08Separate the logical casesL55–56

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L55
    cases hb
  2. L56
    cases hb_right
09Construct an explicit witnessL57–62

Supply the displayed value, then prove that it has the required property.

  1. L57
    exists x3
  2. L58
    exists x4
  3. L59
    exists x2
  4. L60
    exists x10
  5. L61
    exists x11
  6. L62
    exists x12
10Separate the logical casesL63–63

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L63
    split
11Use earlier factsL64–64

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L64
    exact ha
12Separate the logical casesL65–65

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L65
    split
13Use earlier factsL66–66

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L66
    exact hb_right_left
14Separate the logical casesL67–67

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L67
    split
15Use earlier factsL68–68

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L68
    exact hquotient_witness_witness_witness_witness_witness_right_right_left
16Construct an explicit witnessL69–75

Supply the displayed value, then prove that it has the required property.

  1. L69
    exists x
  2. L70
    exists x1
  3. L71
    exists x5
  4. L72
    exists x6
  5. L73
    exists x7
  6. L74
    exists x8
  7. L75
    exists x9
17Separate the logical casesL76–76

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L76
    split
18Use earlier factsL77–77

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L77
    exact hquotient_witness_witness_witness_witness_witness_left
19Separate the logical casesL78–78

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L78
    split
20Use earlier factsL79–79

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L79
    exact hquotient_witness_witness_witness_witness_witness_right_left
21Separate the logical casesL80–80

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L80
    split
22Use earlier factsL81–81

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L81
    exact hquotient_witness_witness_witness_witness_witness_right_right_right
23Separate the logical casesL82–82

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L82
    split
24Use earlier factsL83–83

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L83
    exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_left
25Separate the logical casesL84–84

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L84
    split
26Use earlier factsL85–86

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L85
    exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  2. L86
    exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 86 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro d
  8. 0008intro hp
  9. 0009intro ha
  10. 0010intro hb
  11. 0011have hquotient : exists b k q qb qc. (((((exists ff_h_pfp_division_total_quotient_datahead. ff_h_pfp_division_total_quotient_datahead + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_total_quotient_datahead. bb = ff_q_pfp_division_total_quotient_datahead * S ((S (0)) * bc) + (b))) /\ (((((~((b) = 0)) /\ ((((exists pfa_gap_division_total_quotient_datainversemultiplicationleft. pfa_gap_division_total_quotient_datainversemultiplicationleft + S (b) = (p)) /\ (((exists pfa_gap_division_total_quotient_datainversemultiplicationright. pfa_gap_division_total_quotient_datainversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_division_total_quotient_datainversemultiplicationresultbound. pfa_gap_division_total_quotient_datainversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_total_quotient_datainversemultiplicationresultcongruence pfa_offset_right_division_total_quotient_datainversemultiplicationresultcongruence. ((b) * (k)) + (p) * pfa_offset_left_division_total_quotient_datainversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_total_quotient_datainversemultiplicationresultcongruence)))))))))))) /\ (((((((q)=0) /\ ((exists pfc_gap_division_total_quotient_datalengthshort. pfc_gap_division_total_quotient_datalengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((forall pfd_index_division_total_quotient_dataexecution. (exists pfa_gap_division_total_quotient_dataexecutionbound. pfa_gap_division_total_quotient_dataexecutionbound + S (pfd_index_division_total_quotient_dataexecution) = (q)) -> exists pfd_value_division_total_quotient_dataexecution. ((((exists ff_h_pfp_division_total_quotient_dataexecutionentry. ff_h_pfp_division_total_quotient_dataexecutionentry + S (pfd_value_division_total_quotient_dataexecution) = S ((S (pfd_index_division_total_quotient_dataexecution)) * qc)) /\ exists ff_q_pfp_division_total_quotient_dataexecutionentry. qb = ff_q_pfp_division_total_quotient_dataexecutionentry * S ((S (pfd_index_division_total_quotient_dataexecution)) * qc) + (pfd_value_division_total_quotient_dataexecution))) /\ ((exists pfd_input_division_total_quotient_dataexecutionstep pfd_previous_division_total_quotient_dataexecutionstep pfd_difference_division_total_quotient_dataexecutionstep. ((((exists ff_h_pfp_division_total_quotient_dataexecutionstepinput. ff_h_pfp_division_total_quotient_dataexecutionstepinput + S (pfd_input_division_total_quotient_dataexecutionstep) = S ((S (pfd_index_division_total_quotient_dataexecution)) * ac)) /\ exists ff_q_pfp_division_total_quotient_dataexecutionstepinput. ab = ff_q_pfp_division_total_quotient_dataexecutionstepinput * S ((S (pfd_index_division_total_quotient_dataexecution)) * ac) + (pfd_input_division_total_quotient_dataexecutionstep))) /\ (((exists pfc_terms_code_division_total_quotient_dataexecutionstepprevious pfc_terms_scale_division_total_quotient_dataexecutionstepprevious pfc_natural_sum_division_total_quotient_dataexecutionstepprevious. ((forall pfc_index_division_total_quotient_dataexecutionsteppreviousdiagonal. (exists pfa_gap_division_total_quotient_dataexecutionsteppreviousdiagonalbound. pfa_gap_division_total_quotient_dataexecutionsteppreviousdiagonalbound + S (pfc_index_division_total_quotient_dataexecutionsteppreviousdiagonal) = (S (pfd_index_division_total_quotient_dataexecution))) -> exists pfc_value_division_total_quotient_dataexecutionsteppreviousdiagonal. ((((exists ff_h_pfp_division_total_quotient_dataexecutionsteppreviousdiagonalentry. ff_h_pfp_division_total_quotient_dataexecutionsteppreviousdiagonalentry + S (pfc_value_division_total_quotient_dataexecutionsteppreviousdiagonal) = S ((S (pfc_index_division_total_quotient_dataexecutionsteppreviousdiagonal)) * pfc_terms_scale_division_total_quotient_dataexecutionstepprevious)) /\ exists ff_q_pfp_division_total_quotient_dataexecutionsteppreviousdiagonalentry. pfc_terms_code_division_total_quotient_dataexecutionstepprevious = ff_q_pfp_division_total_quotient_dataexecutionsteppreviousdiagonalentry * S ((S (pfc_index_division_total_quotient_dataexecutionsteppreviousdiagonal)) * pfc_terms_scale_division_total_quotient_dataexecutionstepprevious) + (pfc_value_division_total_quotient_dataexecutionsteppreviousdiagonal))) /\ ((exists pfc_complement_division_total_quotient_dataexecutionsteppreviousdiagonalterm pfc_left_division_total_quotient_dataexecutionsteppreviousdiagonalterm pfc_right_division_total_quotient_dataexecutionsteppreviousdiagonalterm. (((pfc_index_division_total_quotient_dataexecutionsteppreviousdiagonal)+pfc_complement_division_total_quotient_dataexecutionsteppreviousdiagonalterm=(pfd_index_division_total_quotient_dataexecution)) /\ ((((((exists pfa_gap_division_total_quotient_dataexecutionsteppreviousdiagonaltermleftinside. pfa_gap_division_total_quotient_dataexecutionsteppreviousdiagonaltermleftinside + S (pfc_index_division_total_quotient_dataexecutionsteppreviousdiagonal) = (pfd_index_division_total_quotient_dataexecution)) /\ ((((exists ff_h_pfp_division_total_quotient_dataexecutionsteppreviousdiagonaltermleftentry. ff_h_pfp_division_total_quotient_dataexecutionsteppreviousdiagonaltermleftentry + S (pfc_left_division_total_quotient_dataexecutionsteppreviousdiagonalterm) = S ((S (pfc_index_division_total_quotient_dataexecutionsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_total_quotient_dataexecutionsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_total_quotient_dataexecutionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_total_quotient_dataexecutionsteppreviousdiagonal)) * qc) + (pfc_left_division_total_quotient_dataexecutionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_total_quotient_dataexecutionsteppreviousdiagonaltermleftoutside. pfc_gap_division_total_quotient_dataexecutionsteppreviousdiagonaltermleftoutside+(pfd_index_division_total_quotient_dataexecution)=(pfc_index_division_total_quotient_dataexecutionsteppreviousdiagonal)) /\ (((pfc_left_division_total_quotient_dataexecutionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_total_quotient_dataexecutionsteppreviousdiagonaltermrightinside. pfa_gap_division_total_quotient_dataexecutionsteppreviousdiagonaltermrightinside + S (pfc_complement_division_total_quotient_dataexecutionsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_total_quotient_dataexecutionsteppreviousdiagonaltermrightentry. ff_h_pfp_division_total_quotient_dataexecutionsteppreviousdiagonaltermrightentry + S (pfc_right_division_total_quotient_dataexecutionsteppreviousdiagonalterm) = S ((S (pfc_complement_division_total_quotient_dataexecutionsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_total_quotient_dataexecutionsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_total_quotient_dataexecutionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_total_quotient_dataexecutionsteppreviousdiagonalterm)) * bc) + (pfc_right_division_total_quotient_dataexecutionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_total_quotient_dataexecutionsteppreviousdiagonaltermrightoutside. pfc_gap_division_total_quotient_dataexecutionsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_division_total_quotient_dataexecutionsteppreviousdiagonalterm)) /\ (((pfc_right_division_total_quotient_dataexecutionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_total_quotient_dataexecutionsteppreviousdiagonal)=pfc_left_division_total_quotient_dataexecutionsteppreviousdiagonalterm*pfc_right_division_total_quotient_dataexecutionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_total_quotient_dataexecutionstepprevioussum fs_v_pfc_division_total_quotient_dataexecutionstepprevioussum. ((((exists fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_start. fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_total_quotient_dataexecutionstepprevioussum)) /\ exists fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_start. fs_u_pfc_division_total_quotient_dataexecutionstepprevioussum = fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_total_quotient_dataexecutionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_terminal. fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_terminal + S (pfc_natural_sum_division_total_quotient_dataexecutionstepprevious) = S ((S (S (pfd_index_division_total_quotient_dataexecution))) * fs_v_pfc_division_total_quotient_dataexecutionstepprevioussum)) /\ exists fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_terminal. fs_u_pfc_division_total_quotient_dataexecutionstepprevioussum = fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_terminal * S ((S (S (pfd_index_division_total_quotient_dataexecution))) * fs_v_pfc_division_total_quotient_dataexecutionstepprevioussum) + (pfc_natural_sum_division_total_quotient_dataexecutionstepprevious))) /\ forall fs_i_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps. (exists fs_lt_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_bound. fs_lt_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_bound + S fs_i_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps = S (pfd_index_division_total_quotient_dataexecution)) -> exists fs_a_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps fs_r_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps fs_s_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps. ((((exists fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_summand. fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_summand + S (fs_a_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps)) * pfc_terms_scale_division_total_quotient_dataexecutionstepprevious)) /\ exists fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_summand. pfc_terms_code_division_total_quotient_dataexecutionstepprevious = fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps)) * pfc_terms_scale_division_total_quotient_dataexecutionstepprevious) + (fs_a_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_partial. fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_partial + S (fs_r_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps)) * fs_v_pfc_division_total_quotient_dataexecutionstepprevioussum)) /\ exists fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_partial. fs_u_pfc_division_total_quotient_dataexecutionstepprevioussum = fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps)) * fs_v_pfc_division_total_quotient_dataexecutionstepprevioussum) + (fs_r_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_successor. fs_h_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_successor + S (fs_s_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps)) * fs_v_pfc_division_total_quotient_dataexecutionstepprevioussum)) /\ exists fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_successor. fs_u_pfc_division_total_quotient_dataexecutionstepprevioussum = fs_q_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps)) * fs_v_pfc_division_total_quotient_dataexecutionstepprevioussum) + (fs_s_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps))) /\ fs_s_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps = fs_r_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps + fs_a_pfc_division_total_quotient_dataexecutionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_total_quotient_dataexecutionsteppreviousresiduebound. pfa_gap_division_total_quotient_dataexecutionsteppreviousresiduebound + S (pfd_previous_division_total_quotient_dataexecutionstep) = (p)) /\ ((exists pfa_offset_left_division_total_quotient_dataexecutionsteppreviousresiduecongruence pfa_offset_right_division_total_quotient_dataexecutionsteppreviousresiduecongruence. (pfc_natural_sum_division_total_quotient_dataexecutionstepprevious) + (p) * pfa_offset_left_division_total_quotient_dataexecutionsteppreviousresiduecongruence = (pfd_previous_division_total_quotient_dataexecutionstep) + (p) * pfa_offset_right_division_total_quotient_dataexecutionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_total_quotient_dataexecutionstepsubtractleft. pfa_gap_division_total_quotient_dataexecutionstepsubtractleft + S (pfd_previous_division_total_quotient_dataexecutionstep) = (p)) /\ (((exists pfa_gap_division_total_quotient_dataexecutionstepsubtractright. pfa_gap_division_total_quotient_dataexecutionstepsubtractright + S (pfd_difference_division_total_quotient_dataexecutionstep) = (p)) /\ ((((exists pfa_gap_division_total_quotient_dataexecutionstepsubtractresultbound. pfa_gap_division_total_quotient_dataexecutionstepsubtractresultbound + S (pfd_input_division_total_quotient_dataexecutionstep) = (p)) /\ ((exists pfa_offset_left_division_total_quotient_dataexecutionstepsubtractresultcongruence pfa_offset_right_division_total_quotient_dataexecutionstepsubtractresultcongruence. ((pfd_previous_division_total_quotient_dataexecutionstep) + (pfd_difference_division_total_quotient_dataexecutionstep)) + (p) * pfa_offset_left_division_total_quotient_dataexecutionstepsubtractresultcongruence = (pfd_input_division_total_quotient_dataexecutionstep) + (p) * pfa_offset_right_division_total_quotient_dataexecutionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_total_quotient_dataexecutionstepmultiplyleft. pfa_gap_division_total_quotient_dataexecutionstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_total_quotient_dataexecutionstepmultiplyright. pfa_gap_division_total_quotient_dataexecutionstepmultiplyright + S (pfd_difference_division_total_quotient_dataexecutionstep) = (p)) /\ ((((exists pfa_gap_division_total_quotient_dataexecutionstepmultiplyresultbound. pfa_gap_division_total_quotient_dataexecutionstepmultiplyresultbound + S (pfd_value_division_total_quotient_dataexecution) = (p)) /\ ((exists pfa_offset_left_division_total_quotient_dataexecutionstepmultiplyresultcongruence pfa_offset_right_division_total_quotient_dataexecutionstepmultiplyresultcongruence. ((k) * (pfd_difference_division_total_quotient_dataexecutionstep)) + (p) * pfa_offset_left_division_total_quotient_dataexecutionstepmultiplyresultcongruence = (pfd_value_division_total_quotient_dataexecution) + (p) * pfa_offset_right_division_total_quotient_dataexecutionstepmultiplyresultcongruence))))))))))))))))))))))))))
  12. 0012specialize prime_field_polynomial_division_quotient_data_exists (p)
  13. 0013specialize prime_field_polynomial_division_quotient_data_exists (ab)
  14. 0014specialize prime_field_polynomial_division_quotient_data_exists (ac)
  15. 0015specialize prime_field_polynomial_division_quotient_data_exists (L)
  16. 0016specialize prime_field_polynomial_division_quotient_data_exists (bb)
  17. 0017specialize prime_field_polynomial_division_quotient_data_exists (bc)
  18. 0018specialize prime_field_polynomial_division_quotient_data_exists (d)
  19. 0019apply prime_field_polynomial_division_quotient_data_exists
  20. 0020exact hp
  21. 0021exact ha
  22. 0022exact hb
  23. 0023cases hquotient
  24. 0024cases hquotient_witness
  25. 0025cases hquotient_witness_witness
  26. 0026cases hquotient_witness_witness_witness
  27. 0027cases hquotient_witness_witness_witness_witness
  28. 0028cases hquotient_witness_witness_witness_witness_witness
  29. 0029cases hquotient_witness_witness_witness_witness_witness_right
  30. 0030cases hquotient_witness_witness_witness_witness_witness_right_right
  31. 0031have hresidual : exists pb pc ub uc t rb rc R. (((forall pfc_index_division_total_residual_dataproduct. (exists pfa_gap_division_total_residual_dataproductbound. pfa_gap_division_total_residual_dataproductbound + S (pfc_index_division_total_residual_dataproduct) = (L)) -> exists pfc_value_division_total_residual_dataproduct. ((((exists ff_h_pfp_division_total_residual_dataproductentry. ff_h_pfp_division_total_residual_dataproductentry + S (pfc_value_division_total_residual_dataproduct) = S ((S (pfc_index_division_total_residual_dataproduct)) * pc)) /\ exists ff_q_pfp_division_total_residual_dataproductentry. pb = ff_q_pfp_division_total_residual_dataproductentry * S ((S (pfc_index_division_total_residual_dataproduct)) * pc) + (pfc_value_division_total_residual_dataproduct))) /\ ((exists pfc_terms_code_division_total_residual_dataproductcoefficient pfc_terms_scale_division_total_residual_dataproductcoefficient pfc_natural_sum_division_total_residual_dataproductcoefficient. ((forall pfc_index_division_total_residual_dataproductcoefficientdiagonal. (exists pfa_gap_division_total_residual_dataproductcoefficientdiagonalbound. pfa_gap_division_total_residual_dataproductcoefficientdiagonalbound + S (pfc_index_division_total_residual_dataproductcoefficientdiagonal) = (S (pfc_index_division_total_residual_dataproduct))) -> exists pfc_value_division_total_residual_dataproductcoefficientdiagonal. ((((exists ff_h_pfp_division_total_residual_dataproductcoefficientdiagonalentry. ff_h_pfp_division_total_residual_dataproductcoefficientdiagonalentry + S (pfc_value_division_total_residual_dataproductcoefficientdiagonal) = S ((S (pfc_index_division_total_residual_dataproductcoefficientdiagonal)) * pfc_terms_scale_division_total_residual_dataproductcoefficient)) /\ exists ff_q_pfp_division_total_residual_dataproductcoefficientdiagonalentry. pfc_terms_code_division_total_residual_dataproductcoefficient = ff_q_pfp_division_total_residual_dataproductcoefficientdiagonalentry * S ((S (pfc_index_division_total_residual_dataproductcoefficientdiagonal)) * pfc_terms_scale_division_total_residual_dataproductcoefficient) + (pfc_value_division_total_residual_dataproductcoefficientdiagonal))) /\ ((exists pfc_complement_division_total_residual_dataproductcoefficientdiagonalterm pfc_left_division_total_residual_dataproductcoefficientdiagonalterm pfc_right_division_total_residual_dataproductcoefficientdiagonalterm. (((pfc_index_division_total_residual_dataproductcoefficientdiagonal)+pfc_complement_division_total_residual_dataproductcoefficientdiagonalterm=(pfc_index_division_total_residual_dataproduct)) /\ ((((((exists pfa_gap_division_total_residual_dataproductcoefficientdiagonaltermleftinside. pfa_gap_division_total_residual_dataproductcoefficientdiagonaltermleftinside + S (pfc_index_division_total_residual_dataproductcoefficientdiagonal) = (x2)) /\ ((((exists ff_h_pfp_division_total_residual_dataproductcoefficientdiagonaltermleftentry. ff_h_pfp_division_total_residual_dataproductcoefficientdiagonaltermleftentry + S (pfc_left_division_total_residual_dataproductcoefficientdiagonalterm) = S ((S (pfc_index_division_total_residual_dataproductcoefficientdiagonal)) * x4)) /\ exists ff_q_pfp_division_total_residual_dataproductcoefficientdiagonaltermleftentry. x3 = ff_q_pfp_division_total_residual_dataproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_total_residual_dataproductcoefficientdiagonal)) * x4) + (pfc_left_division_total_residual_dataproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_total_residual_dataproductcoefficientdiagonaltermleftoutside. pfc_gap_division_total_residual_dataproductcoefficientdiagonaltermleftoutside+(x2)=(pfc_index_division_total_residual_dataproductcoefficientdiagonal)) /\ (((pfc_left_division_total_residual_dataproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_total_residual_dataproductcoefficientdiagonaltermrightinside. pfa_gap_division_total_residual_dataproductcoefficientdiagonaltermrightinside + S (pfc_complement_division_total_residual_dataproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_total_residual_dataproductcoefficientdiagonaltermrightentry. ff_h_pfp_division_total_residual_dataproductcoefficientdiagonaltermrightentry + S (pfc_right_division_total_residual_dataproductcoefficientdiagonalterm) = S ((S (pfc_complement_division_total_residual_dataproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_total_residual_dataproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_total_residual_dataproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_total_residual_dataproductcoefficientdiagonalterm)) * bc) + (pfc_right_division_total_residual_dataproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_total_residual_dataproductcoefficientdiagonaltermrightoutside. pfc_gap_division_total_residual_dataproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_total_residual_dataproductcoefficientdiagonalterm)) /\ (((pfc_right_division_total_residual_dataproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_total_residual_dataproductcoefficientdiagonal)=pfc_left_division_total_residual_dataproductcoefficientdiagonalterm*pfc_right_division_total_residual_dataproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_total_residual_dataproductcoefficientsum fs_v_pfc_division_total_residual_dataproductcoefficientsum. ((((exists fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_start. fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_total_residual_dataproductcoefficientsum)) /\ exists fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_start. fs_u_pfc_division_total_residual_dataproductcoefficientsum = fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_total_residual_dataproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_terminal. fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_terminal + S (pfc_natural_sum_division_total_residual_dataproductcoefficient) = S ((S (S (pfc_index_division_total_residual_dataproduct))) * fs_v_pfc_division_total_residual_dataproductcoefficientsum)) /\ exists fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_terminal. fs_u_pfc_division_total_residual_dataproductcoefficientsum = fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_terminal * S ((S (S (pfc_index_division_total_residual_dataproduct))) * fs_v_pfc_division_total_residual_dataproductcoefficientsum) + (pfc_natural_sum_division_total_residual_dataproductcoefficient))) /\ forall fs_i_pfc_division_total_residual_dataproductcoefficientsum_body_steps. (exists fs_lt_pfc_division_total_residual_dataproductcoefficientsum_body_steps_bound. fs_lt_pfc_division_total_residual_dataproductcoefficientsum_body_steps_bound + S fs_i_pfc_division_total_residual_dataproductcoefficientsum_body_steps = S (pfc_index_division_total_residual_dataproduct)) -> exists fs_a_pfc_division_total_residual_dataproductcoefficientsum_body_steps fs_r_pfc_division_total_residual_dataproductcoefficientsum_body_steps fs_s_pfc_division_total_residual_dataproductcoefficientsum_body_steps. ((((exists fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_steps_summand. fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_steps_summand + S (fs_a_pfc_division_total_residual_dataproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_total_residual_dataproductcoefficientsum_body_steps)) * pfc_terms_scale_division_total_residual_dataproductcoefficient)) /\ exists fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_steps_summand. pfc_terms_code_division_total_residual_dataproductcoefficient = fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_total_residual_dataproductcoefficientsum_body_steps)) * pfc_terms_scale_division_total_residual_dataproductcoefficient) + (fs_a_pfc_division_total_residual_dataproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_steps_partial. fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_steps_partial + S (fs_r_pfc_division_total_residual_dataproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_total_residual_dataproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_residual_dataproductcoefficientsum)) /\ exists fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_steps_partial. fs_u_pfc_division_total_residual_dataproductcoefficientsum = fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_total_residual_dataproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_residual_dataproductcoefficientsum) + (fs_r_pfc_division_total_residual_dataproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_steps_successor. fs_h_pfc_division_total_residual_dataproductcoefficientsum_body_steps_successor + S (fs_s_pfc_division_total_residual_dataproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_total_residual_dataproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_residual_dataproductcoefficientsum)) /\ exists fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_steps_successor. fs_u_pfc_division_total_residual_dataproductcoefficientsum = fs_q_pfc_division_total_residual_dataproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_total_residual_dataproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_residual_dataproductcoefficientsum) + (fs_s_pfc_division_total_residual_dataproductcoefficientsum_body_steps))) /\ fs_s_pfc_division_total_residual_dataproductcoefficientsum_body_steps = fs_r_pfc_division_total_residual_dataproductcoefficientsum_body_steps + fs_a_pfc_division_total_residual_dataproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_total_residual_dataproductcoefficientresiduebound. pfa_gap_division_total_residual_dataproductcoefficientresiduebound + S (pfc_value_division_total_residual_dataproduct) = (p)) /\ ((exists pfa_offset_left_division_total_residual_dataproductcoefficientresiduecongruence pfa_offset_right_division_total_residual_dataproductcoefficientresiduecongruence. (pfc_natural_sum_division_total_residual_dataproductcoefficient) + (p) * pfa_offset_left_division_total_residual_dataproductcoefficientresiduecongruence = (pfc_value_division_total_residual_dataproduct) + (p) * pfa_offset_right_division_total_residual_dataproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_division_total_residual_datadifference. (exists pfa_gap_division_total_residual_datadifferenceindex. pfa_gap_division_total_residual_datadifferenceindex + S (pfs_index_division_total_residual_datadifference) = (L)) -> exists pfs_left_division_total_residual_datadifference pfs_right_division_total_residual_datadifference pfs_result_division_total_residual_datadifference. ((((exists ff_h_pfp_division_total_residual_datadifferenceleft. ff_h_pfp_division_total_residual_datadifferenceleft + S (pfs_left_division_total_residual_datadifference) = S ((S (pfs_index_division_total_residual_datadifference)) * ac)) /\ exists ff_q_pfp_division_total_residual_datadifferenceleft. ab = ff_q_pfp_division_total_residual_datadifferenceleft * S ((S (pfs_index_division_total_residual_datadifference)) * ac) + (pfs_left_division_total_residual_datadifference))) /\ (((((exists ff_h_pfp_division_total_residual_datadifferenceright. ff_h_pfp_division_total_residual_datadifferenceright + S (pfs_right_division_total_residual_datadifference) = S ((S (pfs_index_division_total_residual_datadifference)) * pc)) /\ exists ff_q_pfp_division_total_residual_datadifferenceright. pb = ff_q_pfp_division_total_residual_datadifferenceright * S ((S (pfs_index_division_total_residual_datadifference)) * pc) + (pfs_right_division_total_residual_datadifference))) /\ (((((exists ff_h_pfp_division_total_residual_datadifferenceresult. ff_h_pfp_division_total_residual_datadifferenceresult + S (pfs_result_division_total_residual_datadifference) = S ((S (pfs_index_division_total_residual_datadifference)) * uc)) /\ exists ff_q_pfp_division_total_residual_datadifferenceresult. ub = ff_q_pfp_division_total_residual_datadifferenceresult * S ((S (pfs_index_division_total_residual_datadifference)) * uc) + (pfs_result_division_total_residual_datadifference))) /\ ((((exists pfa_gap_division_total_residual_datadifferenceoperationleft. pfa_gap_division_total_residual_datadifferenceoperationleft + S (pfs_right_division_total_residual_datadifference) = (p)) /\ (((exists pfa_gap_division_total_residual_datadifferenceoperationright. pfa_gap_division_total_residual_datadifferenceoperationright + S (pfs_result_division_total_residual_datadifference) = (p)) /\ ((((exists pfa_gap_division_total_residual_datadifferenceoperationresultbound. pfa_gap_division_total_residual_datadifferenceoperationresultbound + S (pfs_left_division_total_residual_datadifference) = (p)) /\ ((exists pfa_offset_left_division_total_residual_datadifferenceoperationresultcongruence pfa_offset_right_division_total_residual_datadifferenceoperationresultcongruence. ((pfs_right_division_total_residual_datadifference) + (pfs_result_division_total_residual_datadifference)) + (p) * pfa_offset_left_division_total_residual_datadifferenceoperationresultcongruence = (pfs_left_division_total_residual_datadifference) + (p) * pfa_offset_right_division_total_residual_datadifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(t)+(R)) /\ (((forall fom_index_pfp_division_total_residual_datatriminput. (exists fom_gap_pfp_division_total_residual_datatriminput_index_bound. fom_gap_pfp_division_total_residual_datatriminput_index_bound + S (fom_index_pfp_division_total_residual_datatriminput) = L) -> exists fom_value_pfp_division_total_residual_datatriminput. ((((exists fom_beta_height_pfp_division_total_residual_datatriminput_entry. fom_beta_height_pfp_division_total_residual_datatriminput_entry + S (fom_value_pfp_division_total_residual_datatriminput) = S ((S (fom_index_pfp_division_total_residual_datatriminput)) * uc)) /\ exists fom_beta_quotient_pfp_division_total_residual_datatriminput_entry. ub = fom_beta_quotient_pfp_division_total_residual_datatriminput_entry * S ((S (fom_index_pfp_division_total_residual_datatriminput)) * uc) + (fom_value_pfp_division_total_residual_datatriminput))) /\ (exists fom_gap_pfp_division_total_residual_datatriminput_value_bound. fom_gap_pfp_division_total_residual_datatriminput_value_bound + S (fom_value_pfp_division_total_residual_datatriminput) = p))) /\ (((forall pfp_repeat_index_division_total_residual_datatrimremoved. (exists pfa_gap_division_total_residual_datatrimremovedindex. pfa_gap_division_total_residual_datatrimremovedindex + S (pfp_repeat_index_division_total_residual_datatrimremoved) = (t)) -> (((exists ff_h_pfp_division_total_residual_datatrimremovedentry. ff_h_pfp_division_total_residual_datatrimremovedentry + S (0) = S ((S (pfp_repeat_index_division_total_residual_datatrimremoved)) * uc)) /\ exists ff_q_pfp_division_total_residual_datatrimremovedentry. ub = ff_q_pfp_division_total_residual_datatrimremovedentry * S ((S (pfp_repeat_index_division_total_residual_datatrimremoved)) * uc) + (0)))) /\ (((forall pftrim_index_division_total_residual_datatrimsuffix pftrim_value_division_total_residual_datatrimsuffix. (exists pfa_gap_division_total_residual_datatrimsuffixbound. pfa_gap_division_total_residual_datatrimsuffixbound + S (pftrim_index_division_total_residual_datatrimsuffix) = (R)) -> (((exists ff_h_pfp_division_total_residual_datatrimsuffixsource. ff_h_pfp_division_total_residual_datatrimsuffixsource + S (pftrim_value_division_total_residual_datatrimsuffix) = S ((S ((t)+pftrim_index_division_total_residual_datatrimsuffix)) * uc)) /\ exists ff_q_pfp_division_total_residual_datatrimsuffixsource. ub = ff_q_pfp_division_total_residual_datatrimsuffixsource * S ((S ((t)+pftrim_index_division_total_residual_datatrimsuffix)) * uc) + (pftrim_value_division_total_residual_datatrimsuffix))) -> (((exists ff_h_pfp_division_total_residual_datatrimsuffixoutput. ff_h_pfp_division_total_residual_datatrimsuffixoutput + S (pftrim_value_division_total_residual_datatrimsuffix) = S ((S (pftrim_index_division_total_residual_datatrimsuffix)) * rc)) /\ exists ff_q_pfp_division_total_residual_datatrimsuffixoutput. rb = ff_q_pfp_division_total_residual_datatrimsuffixoutput * S ((S (pftrim_index_division_total_residual_datatrimsuffix)) * rc) + (pftrim_value_division_total_residual_datatrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_total_residual_datatrimnormal. ((((exists ff_h_pfp_division_total_residual_datatrimnormalentry. ff_h_pfp_division_total_residual_datatrimnormalentry + S (pftrim_leading_division_total_residual_datatrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_total_residual_datatrimnormalentry. rb = ff_q_pfp_division_total_residual_datatrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_total_residual_datatrimnormal))) /\ ((~(pftrim_leading_division_total_residual_datatrimnormal=0))))))))))))))))))))
  32. 0032specialize prime_field_polynomial_division_residual_data_exists (p)
  33. 0033specialize prime_field_polynomial_division_residual_data_exists (ab)
  34. 0034specialize prime_field_polynomial_division_residual_data_exists (ac)
  35. 0035specialize prime_field_polynomial_division_residual_data_exists (L)
  36. 0036specialize prime_field_polynomial_division_residual_data_exists (bb)
  37. 0037specialize prime_field_polynomial_division_residual_data_exists (bc)
  38. 0038specialize prime_field_polynomial_division_residual_data_exists (d)
  39. 0039specialize prime_field_polynomial_division_residual_data_exists (x3)
  40. 0040specialize prime_field_polynomial_division_residual_data_exists (x4)
  41. 0041specialize prime_field_polynomial_division_residual_data_exists (x2)
  42. 0042apply prime_field_polynomial_division_residual_data_exists
  43. 0043exact hp
  44. 0044exact ha
  45. 0045cases hresidual
  46. 0046cases hresidual_witness
  47. 0047cases hresidual_witness_witness
  48. 0048cases hresidual_witness_witness_witness
  49. 0049cases hresidual_witness_witness_witness_witness
  50. 0050cases hresidual_witness_witness_witness_witness_witness
  51. 0051cases hresidual_witness_witness_witness_witness_witness_witness
  52. 0052cases hresidual_witness_witness_witness_witness_witness_witness_witness
  53. 0053cases hresidual_witness_witness_witness_witness_witness_witness_witness_witness
  54. 0054cases hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right
  55. 0055cases hb
  56. 0056cases hb_right
  57. 0057exists x3
  58. 0058exists x4
  59. 0059exists x2
  60. 0060exists x10
  61. 0061exists x11
  62. 0062exists x12
  63. 0063split
  64. 0064exact ha
  65. 0065split
  66. 0066exact hb_right_left
  67. 0067split
  68. 0068exact hquotient_witness_witness_witness_witness_witness_right_right_left
  69. 0069exists x
  70. 0070exists x1
  71. 0071exists x5
  72. 0072exists x6
  73. 0073exists x7
  74. 0074exists x8
  75. 0075exists x9
  76. 0076split
  77. 0077exact hquotient_witness_witness_witness_witness_witness_left
  78. 0078split
  79. 0079exact hquotient_witness_witness_witness_witness_witness_right_left
  80. 0080split
  81. 0081exact hquotient_witness_witness_witness_witness_witness_right_right_right
  82. 0082split
  83. 0083exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_left
  84. 0084split
  85. 0085exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  86. 0086exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right_right