PX003B

prime_field_polynomial_division_exists_with_remainder_bound

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

Unconditionally construct an actual general division execution and derive its strict remainder-degree alternative; no theorem claims degree for zero.

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_bounded_prime pfa_factor_right_division_bounded_prime. (p) = pfa_factor_left_division_bounded_prime * pfa_factor_right_division_bounded_prime -> pfa_factor_left_division_bounded_prime = 1 \/ pfa_factor_right_division_bounded_prime = 1) -> (forall fom_index_pfp_division_bounded_input. (exists fom_gap_pfp_division_bounded_input_index_bound. fom_gap_pfp_division_bounded_input_index_bound + S (fom_index_pfp_division_bounded_input) = L) -> exists fom_value_pfp_division_bounded_input. ((((exists fom_beta_height_pfp_division_bounded_input_entry. fom_beta_height_pfp_division_bounded_input_entry + S (fom_value_pfp_division_bounded_input) = S ((S (fom_index_pfp_division_bounded_input)) * ac)) /\ exists fom_beta_quotient_pfp_division_bounded_input_entry. ab = fom_beta_quotient_pfp_division_bounded_input_entry * S ((S (fom_index_pfp_division_bounded_input)) * ac) + (fom_value_pfp_division_bounded_input))) /\ (exists fom_gap_pfp_division_bounded_input_value_bound. fom_gap_pfp_division_bounded_input_value_bound + S (fom_value_pfp_division_bounded_input) = p))) -> ((((S d)=S (d)) /\ (((forall fom_index_pfp_division_bounded_divisorcoefficients. (exists fom_gap_pfp_division_bounded_divisorcoefficients_index_bound. fom_gap_pfp_division_bounded_divisorcoefficients_index_bound + S (fom_index_pfp_division_bounded_divisorcoefficients) = S d) -> exists fom_value_pfp_division_bounded_divisorcoefficients. ((((exists fom_beta_height_pfp_division_bounded_divisorcoefficients_entry. fom_beta_height_pfp_division_bounded_divisorcoefficients_entry + S (fom_value_pfp_division_bounded_divisorcoefficients) = S ((S (fom_index_pfp_division_bounded_divisorcoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_division_bounded_divisorcoefficients_entry. bb = fom_beta_quotient_pfp_division_bounded_divisorcoefficients_entry * S ((S (fom_index_pfp_division_bounded_divisorcoefficients)) * bc) + (fom_value_pfp_division_bounded_divisorcoefficients))) /\ (exists fom_gap_pfp_division_bounded_divisorcoefficients_value_bound. fom_gap_pfp_division_bounded_divisorcoefficients_value_bound + S (fom_value_pfp_division_bounded_divisorcoefficients) = p))) /\ ((exists pfd_leading_division_bounded_divisor. ((((exists ff_h_pfp_division_bounded_divisorentry. ff_h_pfp_division_bounded_divisorentry + S (pfd_leading_division_bounded_divisor) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_bounded_divisorentry. bb = ff_q_pfp_division_bounded_divisorentry * S ((S (0)) * bc) + (pfd_leading_division_bounded_divisor))) /\ ((~(pfd_leading_division_bounded_divisor=0)))))))))) -> exists qb qc q rb rc R. ((((forall fom_index_pfp_division_bounded_executioninput. (exists fom_gap_pfp_division_bounded_executioninput_index_bound. fom_gap_pfp_division_bounded_executioninput_index_bound + S (fom_index_pfp_division_bounded_executioninput) = L) -> exists fom_value_pfp_division_bounded_executioninput. ((((exists fom_beta_height_pfp_division_bounded_executioninput_entry. fom_beta_height_pfp_division_bounded_executioninput_entry + S (fom_value_pfp_division_bounded_executioninput) = S ((S (fom_index_pfp_division_bounded_executioninput)) * ac)) /\ exists fom_beta_quotient_pfp_division_bounded_executioninput_entry. ab = fom_beta_quotient_pfp_division_bounded_executioninput_entry * S ((S (fom_index_pfp_division_bounded_executioninput)) * ac) + (fom_value_pfp_division_bounded_executioninput))) /\ (exists fom_gap_pfp_division_bounded_executioninput_value_bound. fom_gap_pfp_division_bounded_executioninput_value_bound + S (fom_value_pfp_division_bounded_executioninput) = p))) /\ (((forall fom_index_pfp_division_bounded_executiondivisor. (exists fom_gap_pfp_division_bounded_executiondivisor_index_bound. fom_gap_pfp_division_bounded_executiondivisor_index_bound + S (fom_index_pfp_division_bounded_executiondivisor) = S (d)) -> exists fom_value_pfp_division_bounded_executiondivisor. ((((exists fom_beta_height_pfp_division_bounded_executiondivisor_entry. fom_beta_height_pfp_division_bounded_executiondivisor_entry + S (fom_value_pfp_division_bounded_executiondivisor) = S ((S (fom_index_pfp_division_bounded_executiondivisor)) * bc)) /\ exists fom_beta_quotient_pfp_division_bounded_executiondivisor_entry. bb = fom_beta_quotient_pfp_division_bounded_executiondivisor_entry * S ((S (fom_index_pfp_division_bounded_executiondivisor)) * bc) + (fom_value_pfp_division_bounded_executiondivisor))) /\ (exists fom_gap_pfp_division_bounded_executiondivisor_value_bound. fom_gap_pfp_division_bounded_executiondivisor_value_bound + S (fom_value_pfp_division_bounded_executiondivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_division_bounded_executionlengthshort. pfc_gap_division_bounded_executionlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_division_bounded_execution pfd_inverse_division_bounded_execution pfd_product_code_division_bounded_execution pfd_product_scale_division_bounded_execution pfd_residual_code_division_bounded_execution pfd_residual_scale_division_bounded_execution pfd_cut_division_bounded_execution. ((((exists ff_h_pfp_division_bounded_executionhead. ff_h_pfp_division_bounded_executionhead + S (pfd_head_division_bounded_execution) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_bounded_executionhead. bb = ff_q_pfp_division_bounded_executionhead * S ((S (0)) * bc) + (pfd_head_division_bounded_execution))) /\ (((((~((pfd_head_division_bounded_execution) = 0)) /\ ((((exists pfa_gap_division_bounded_executioninversemultiplicationleft. pfa_gap_division_bounded_executioninversemultiplicationleft + S (pfd_head_division_bounded_execution) = (p)) /\ (((exists pfa_gap_division_bounded_executioninversemultiplicationright. pfa_gap_division_bounded_executioninversemultiplicationright + S (pfd_inverse_division_bounded_execution) = (p)) /\ ((((exists pfa_gap_division_bounded_executioninversemultiplicationresultbound. pfa_gap_division_bounded_executioninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_bounded_executioninversemultiplicationresultcongruence pfa_offset_right_division_bounded_executioninversemultiplicationresultcongruence. ((pfd_head_division_bounded_execution) * (pfd_inverse_division_bounded_execution)) + (p) * pfa_offset_left_division_bounded_executioninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_bounded_executioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_division_bounded_executionquotient. (exists pfa_gap_division_bounded_executionquotientbound. pfa_gap_division_bounded_executionquotientbound + S (pfd_index_division_bounded_executionquotient) = (q)) -> exists pfd_value_division_bounded_executionquotient. ((((exists ff_h_pfp_division_bounded_executionquotiententry. ff_h_pfp_division_bounded_executionquotiententry + S (pfd_value_division_bounded_executionquotient) = S ((S (pfd_index_division_bounded_executionquotient)) * qc)) /\ exists ff_q_pfp_division_bounded_executionquotiententry. qb = ff_q_pfp_division_bounded_executionquotiententry * S ((S (pfd_index_division_bounded_executionquotient)) * qc) + (pfd_value_division_bounded_executionquotient))) /\ ((exists pfd_input_division_bounded_executionquotientstep pfd_previous_division_bounded_executionquotientstep pfd_difference_division_bounded_executionquotientstep. ((((exists ff_h_pfp_division_bounded_executionquotientstepinput. ff_h_pfp_division_bounded_executionquotientstepinput + S (pfd_input_division_bounded_executionquotientstep) = S ((S (pfd_index_division_bounded_executionquotient)) * ac)) /\ exists ff_q_pfp_division_bounded_executionquotientstepinput. ab = ff_q_pfp_division_bounded_executionquotientstepinput * S ((S (pfd_index_division_bounded_executionquotient)) * ac) + (pfd_input_division_bounded_executionquotientstep))) /\ (((exists pfc_terms_code_division_bounded_executionquotientstepprevious pfc_terms_scale_division_bounded_executionquotientstepprevious pfc_natural_sum_division_bounded_executionquotientstepprevious. ((forall pfc_index_division_bounded_executionquotientsteppreviousdiagonal. (exists pfa_gap_division_bounded_executionquotientsteppreviousdiagonalbound. pfa_gap_division_bounded_executionquotientsteppreviousdiagonalbound + S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal) = (S (pfd_index_division_bounded_executionquotient))) -> exists pfc_value_division_bounded_executionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonalentry. ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonalentry + S (pfc_value_division_bounded_executionquotientsteppreviousdiagonal) = S ((S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_division_bounded_executionquotientstepprevious)) /\ exists ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonalentry. pfc_terms_code_division_bounded_executionquotientstepprevious = ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonalentry * S ((S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_division_bounded_executionquotientstepprevious) + (pfc_value_division_bounded_executionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm. (((pfc_index_division_bounded_executionquotientsteppreviousdiagonal)+pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm=(pfd_index_division_bounded_executionquotient)) /\ ((((((exists pfa_gap_division_bounded_executionquotientsteppreviousdiagonaltermleftinside. pfa_gap_division_bounded_executionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal) = (pfd_index_division_bounded_executionquotient)) /\ ((((exists ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) * qc) + (pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_executionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_division_bounded_executionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_division_bounded_executionquotient)=(pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) /\ (((pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_bounded_executionquotientsteppreviousdiagonaltermrightinside. pfa_gap_division_bounded_executionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_executionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_division_bounded_executionquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_bounded_executionquotientsteppreviousdiagonal)=pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm*pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_bounded_executionquotientstepprevioussum fs_v_pfc_division_bounded_executionquotientstepprevioussum. ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_start. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_start. fs_u_pfc_division_bounded_executionquotientstepprevioussum = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_terminal. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_division_bounded_executionquotientstepprevious) = S ((S (S (pfd_index_division_bounded_executionquotient))) * fs_v_pfc_division_bounded_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_terminal. fs_u_pfc_division_bounded_executionquotientstepprevioussum = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_division_bounded_executionquotient))) * fs_v_pfc_division_bounded_executionquotientstepprevioussum) + (pfc_natural_sum_division_bounded_executionquotientstepprevious))) /\ forall fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_division_bounded_executionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_division_bounded_executionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps = S (pfd_index_division_bounded_executionquotient)) -> exists fs_a_pfc_division_bounded_executionquotientstepprevioussum_body_steps fs_r_pfc_division_bounded_executionquotientstepprevioussum_body_steps fs_s_pfc_division_bounded_executionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_summand. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_division_bounded_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_bounded_executionquotientstepprevious)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_summand. pfc_terms_code_division_bounded_executionquotientstepprevious = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_bounded_executionquotientstepprevious) + (fs_a_pfc_division_bounded_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_partial. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_division_bounded_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_partial. fs_u_pfc_division_bounded_executionquotientstepprevioussum = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum) + (fs_r_pfc_division_bounded_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_successor. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_division_bounded_executionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_successor. fs_u_pfc_division_bounded_executionquotientstepprevioussum = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum) + (fs_s_pfc_division_bounded_executionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_division_bounded_executionquotientstepprevioussum_body_steps = fs_r_pfc_division_bounded_executionquotientstepprevioussum_body_steps + fs_a_pfc_division_bounded_executionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_bounded_executionquotientsteppreviousresiduebound. pfa_gap_division_bounded_executionquotientsteppreviousresiduebound + S (pfd_previous_division_bounded_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_division_bounded_executionquotientsteppreviousresiduecongruence pfa_offset_right_division_bounded_executionquotientsteppreviousresiduecongruence. (pfc_natural_sum_division_bounded_executionquotientstepprevious) + (p) * pfa_offset_left_division_bounded_executionquotientsteppreviousresiduecongruence = (pfd_previous_division_bounded_executionquotientstep) + (p) * pfa_offset_right_division_bounded_executionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_bounded_executionquotientstepsubtractleft. pfa_gap_division_bounded_executionquotientstepsubtractleft + S (pfd_previous_division_bounded_executionquotientstep) = (p)) /\ (((exists pfa_gap_division_bounded_executionquotientstepsubtractright. pfa_gap_division_bounded_executionquotientstepsubtractright + S (pfd_difference_division_bounded_executionquotientstep) = (p)) /\ ((((exists pfa_gap_division_bounded_executionquotientstepsubtractresultbound. pfa_gap_division_bounded_executionquotientstepsubtractresultbound + S (pfd_input_division_bounded_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_division_bounded_executionquotientstepsubtractresultcongruence pfa_offset_right_division_bounded_executionquotientstepsubtractresultcongruence. ((pfd_previous_division_bounded_executionquotientstep) + (pfd_difference_division_bounded_executionquotientstep)) + (p) * pfa_offset_left_division_bounded_executionquotientstepsubtractresultcongruence = (pfd_input_division_bounded_executionquotientstep) + (p) * pfa_offset_right_division_bounded_executionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_bounded_executionquotientstepmultiplyleft. pfa_gap_division_bounded_executionquotientstepmultiplyleft + S (pfd_inverse_division_bounded_execution) = (p)) /\ (((exists pfa_gap_division_bounded_executionquotientstepmultiplyright. pfa_gap_division_bounded_executionquotientstepmultiplyright + S (pfd_difference_division_bounded_executionquotientstep) = (p)) /\ ((((exists pfa_gap_division_bounded_executionquotientstepmultiplyresultbound. pfa_gap_division_bounded_executionquotientstepmultiplyresultbound + S (pfd_value_division_bounded_executionquotient) = (p)) /\ ((exists pfa_offset_left_division_bounded_executionquotientstepmultiplyresultcongruence pfa_offset_right_division_bounded_executionquotientstepmultiplyresultcongruence. ((pfd_inverse_division_bounded_execution) * (pfd_difference_division_bounded_executionquotientstep)) + (p) * pfa_offset_left_division_bounded_executionquotientstepmultiplyresultcongruence = (pfd_value_division_bounded_executionquotient) + (p) * pfa_offset_right_division_bounded_executionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_division_bounded_executionproduct. (exists pfa_gap_division_bounded_executionproductbound. pfa_gap_division_bounded_executionproductbound + S (pfc_index_division_bounded_executionproduct) = (L)) -> exists pfc_value_division_bounded_executionproduct. ((((exists ff_h_pfp_division_bounded_executionproductentry. ff_h_pfp_division_bounded_executionproductentry + S (pfc_value_division_bounded_executionproduct) = S ((S (pfc_index_division_bounded_executionproduct)) * pfd_product_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executionproductentry. pfd_product_code_division_bounded_execution = ff_q_pfp_division_bounded_executionproductentry * S ((S (pfc_index_division_bounded_executionproduct)) * pfd_product_scale_division_bounded_execution) + (pfc_value_division_bounded_executionproduct))) /\ ((exists pfc_terms_code_division_bounded_executionproductcoefficient pfc_terms_scale_division_bounded_executionproductcoefficient pfc_natural_sum_division_bounded_executionproductcoefficient. ((forall pfc_index_division_bounded_executionproductcoefficientdiagonal. (exists pfa_gap_division_bounded_executionproductcoefficientdiagonalbound. pfa_gap_division_bounded_executionproductcoefficientdiagonalbound + S (pfc_index_division_bounded_executionproductcoefficientdiagonal) = (S (pfc_index_division_bounded_executionproduct))) -> exists pfc_value_division_bounded_executionproductcoefficientdiagonal. ((((exists ff_h_pfp_division_bounded_executionproductcoefficientdiagonalentry. ff_h_pfp_division_bounded_executionproductcoefficientdiagonalentry + S (pfc_value_division_bounded_executionproductcoefficientdiagonal) = S ((S (pfc_index_division_bounded_executionproductcoefficientdiagonal)) * pfc_terms_scale_division_bounded_executionproductcoefficient)) /\ exists ff_q_pfp_division_bounded_executionproductcoefficientdiagonalentry. pfc_terms_code_division_bounded_executionproductcoefficient = ff_q_pfp_division_bounded_executionproductcoefficientdiagonalentry * S ((S (pfc_index_division_bounded_executionproductcoefficientdiagonal)) * pfc_terms_scale_division_bounded_executionproductcoefficient) + (pfc_value_division_bounded_executionproductcoefficientdiagonal))) /\ ((exists pfc_complement_division_bounded_executionproductcoefficientdiagonalterm pfc_left_division_bounded_executionproductcoefficientdiagonalterm pfc_right_division_bounded_executionproductcoefficientdiagonalterm. (((pfc_index_division_bounded_executionproductcoefficientdiagonal)+pfc_complement_division_bounded_executionproductcoefficientdiagonalterm=(pfc_index_division_bounded_executionproduct)) /\ ((((((exists pfa_gap_division_bounded_executionproductcoefficientdiagonaltermleftinside. pfa_gap_division_bounded_executionproductcoefficientdiagonaltermleftinside + S (pfc_index_division_bounded_executionproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_bounded_executionproductcoefficientdiagonaltermleftentry. ff_h_pfp_division_bounded_executionproductcoefficientdiagonaltermleftentry + S (pfc_left_division_bounded_executionproductcoefficientdiagonalterm) = S ((S (pfc_index_division_bounded_executionproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_bounded_executionproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_bounded_executionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_bounded_executionproductcoefficientdiagonal)) * qc) + (pfc_left_division_bounded_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_executionproductcoefficientdiagonaltermleftoutside. pfc_gap_division_bounded_executionproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_bounded_executionproductcoefficientdiagonal)) /\ (((pfc_left_division_bounded_executionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_bounded_executionproductcoefficientdiagonaltermrightinside. pfa_gap_division_bounded_executionproductcoefficientdiagonaltermrightinside + S (pfc_complement_division_bounded_executionproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_bounded_executionproductcoefficientdiagonaltermrightentry. ff_h_pfp_division_bounded_executionproductcoefficientdiagonaltermrightentry + S (pfc_right_division_bounded_executionproductcoefficientdiagonalterm) = S ((S (pfc_complement_division_bounded_executionproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_bounded_executionproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_bounded_executionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_bounded_executionproductcoefficientdiagonalterm)) * bc) + (pfc_right_division_bounded_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_executionproductcoefficientdiagonaltermrightoutside. pfc_gap_division_bounded_executionproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_bounded_executionproductcoefficientdiagonalterm)) /\ (((pfc_right_division_bounded_executionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_bounded_executionproductcoefficientdiagonal)=pfc_left_division_bounded_executionproductcoefficientdiagonalterm*pfc_right_division_bounded_executionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_bounded_executionproductcoefficientsum fs_v_pfc_division_bounded_executionproductcoefficientsum. ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_start. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_bounded_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_start. fs_u_pfc_division_bounded_executionproductcoefficientsum = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_bounded_executionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_terminal. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_terminal + S (pfc_natural_sum_division_bounded_executionproductcoefficient) = S ((S (S (pfc_index_division_bounded_executionproduct))) * fs_v_pfc_division_bounded_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_terminal. fs_u_pfc_division_bounded_executionproductcoefficientsum = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_division_bounded_executionproduct))) * fs_v_pfc_division_bounded_executionproductcoefficientsum) + (pfc_natural_sum_division_bounded_executionproductcoefficient))) /\ forall fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps. (exists fs_lt_pfc_division_bounded_executionproductcoefficientsum_body_steps_bound. fs_lt_pfc_division_bounded_executionproductcoefficientsum_body_steps_bound + S fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps = S (pfc_index_division_bounded_executionproduct)) -> exists fs_a_pfc_division_bounded_executionproductcoefficientsum_body_steps fs_r_pfc_division_bounded_executionproductcoefficientsum_body_steps fs_s_pfc_division_bounded_executionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_summand. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_division_bounded_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_division_bounded_executionproductcoefficient)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_summand. pfc_terms_code_division_bounded_executionproductcoefficient = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_division_bounded_executionproductcoefficient) + (fs_a_pfc_division_bounded_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_partial. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_division_bounded_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_partial. fs_u_pfc_division_bounded_executionproductcoefficientsum = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_executionproductcoefficientsum) + (fs_r_pfc_division_bounded_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_successor. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_division_bounded_executionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_successor. fs_u_pfc_division_bounded_executionproductcoefficientsum = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_executionproductcoefficientsum) + (fs_s_pfc_division_bounded_executionproductcoefficientsum_body_steps))) /\ fs_s_pfc_division_bounded_executionproductcoefficientsum_body_steps = fs_r_pfc_division_bounded_executionproductcoefficientsum_body_steps + fs_a_pfc_division_bounded_executionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_bounded_executionproductcoefficientresiduebound. pfa_gap_division_bounded_executionproductcoefficientresiduebound + S (pfc_value_division_bounded_executionproduct) = (p)) /\ ((exists pfa_offset_left_division_bounded_executionproductcoefficientresiduecongruence pfa_offset_right_division_bounded_executionproductcoefficientresiduecongruence. (pfc_natural_sum_division_bounded_executionproductcoefficient) + (p) * pfa_offset_left_division_bounded_executionproductcoefficientresiduecongruence = (pfc_value_division_bounded_executionproduct) + (p) * pfa_offset_right_division_bounded_executionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_division_bounded_executiondifference. (exists pfa_gap_division_bounded_executiondifferenceindex. pfa_gap_division_bounded_executiondifferenceindex + S (pfs_index_division_bounded_executiondifference) = (L)) -> exists pfs_left_division_bounded_executiondifference pfs_right_division_bounded_executiondifference pfs_result_division_bounded_executiondifference. ((((exists ff_h_pfp_division_bounded_executiondifferenceleft. ff_h_pfp_division_bounded_executiondifferenceleft + S (pfs_left_division_bounded_executiondifference) = S ((S (pfs_index_division_bounded_executiondifference)) * ac)) /\ exists ff_q_pfp_division_bounded_executiondifferenceleft. ab = ff_q_pfp_division_bounded_executiondifferenceleft * S ((S (pfs_index_division_bounded_executiondifference)) * ac) + (pfs_left_division_bounded_executiondifference))) /\ (((((exists ff_h_pfp_division_bounded_executiondifferenceright. ff_h_pfp_division_bounded_executiondifferenceright + S (pfs_right_division_bounded_executiondifference) = S ((S (pfs_index_division_bounded_executiondifference)) * pfd_product_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executiondifferenceright. pfd_product_code_division_bounded_execution = ff_q_pfp_division_bounded_executiondifferenceright * S ((S (pfs_index_division_bounded_executiondifference)) * pfd_product_scale_division_bounded_execution) + (pfs_right_division_bounded_executiondifference))) /\ (((((exists ff_h_pfp_division_bounded_executiondifferenceresult. ff_h_pfp_division_bounded_executiondifferenceresult + S (pfs_result_division_bounded_executiondifference) = S ((S (pfs_index_division_bounded_executiondifference)) * pfd_residual_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executiondifferenceresult. pfd_residual_code_division_bounded_execution = ff_q_pfp_division_bounded_executiondifferenceresult * S ((S (pfs_index_division_bounded_executiondifference)) * pfd_residual_scale_division_bounded_execution) + (pfs_result_division_bounded_executiondifference))) /\ ((((exists pfa_gap_division_bounded_executiondifferenceoperationleft. pfa_gap_division_bounded_executiondifferenceoperationleft + S (pfs_right_division_bounded_executiondifference) = (p)) /\ (((exists pfa_gap_division_bounded_executiondifferenceoperationright. pfa_gap_division_bounded_executiondifferenceoperationright + S (pfs_result_division_bounded_executiondifference) = (p)) /\ ((((exists pfa_gap_division_bounded_executiondifferenceoperationresultbound. pfa_gap_division_bounded_executiondifferenceoperationresultbound + S (pfs_left_division_bounded_executiondifference) = (p)) /\ ((exists pfa_offset_left_division_bounded_executiondifferenceoperationresultcongruence pfa_offset_right_division_bounded_executiondifferenceoperationresultcongruence. ((pfs_right_division_bounded_executiondifference) + (pfs_result_division_bounded_executiondifference)) + (p) * pfa_offset_left_division_bounded_executiondifferenceoperationresultcongruence = (pfs_left_division_bounded_executiondifference) + (p) * pfa_offset_right_division_bounded_executiondifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_division_bounded_execution)+(R)) /\ (((forall fom_index_pfp_division_bounded_executiontriminput. (exists fom_gap_pfp_division_bounded_executiontriminput_index_bound. fom_gap_pfp_division_bounded_executiontriminput_index_bound + S (fom_index_pfp_division_bounded_executiontriminput) = L) -> exists fom_value_pfp_division_bounded_executiontriminput. ((((exists fom_beta_height_pfp_division_bounded_executiontriminput_entry. fom_beta_height_pfp_division_bounded_executiontriminput_entry + S (fom_value_pfp_division_bounded_executiontriminput) = S ((S (fom_index_pfp_division_bounded_executiontriminput)) * pfd_residual_scale_division_bounded_execution)) /\ exists fom_beta_quotient_pfp_division_bounded_executiontriminput_entry. pfd_residual_code_division_bounded_execution = fom_beta_quotient_pfp_division_bounded_executiontriminput_entry * S ((S (fom_index_pfp_division_bounded_executiontriminput)) * pfd_residual_scale_division_bounded_execution) + (fom_value_pfp_division_bounded_executiontriminput))) /\ (exists fom_gap_pfp_division_bounded_executiontriminput_value_bound. fom_gap_pfp_division_bounded_executiontriminput_value_bound + S (fom_value_pfp_division_bounded_executiontriminput) = p))) /\ (((forall pfp_repeat_index_division_bounded_executiontrimremoved. (exists pfa_gap_division_bounded_executiontrimremovedindex. pfa_gap_division_bounded_executiontrimremovedindex + S (pfp_repeat_index_division_bounded_executiontrimremoved) = (pfd_cut_division_bounded_execution)) -> (((exists ff_h_pfp_division_bounded_executiontrimremovedentry. ff_h_pfp_division_bounded_executiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_division_bounded_executiontrimremoved)) * pfd_residual_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executiontrimremovedentry. pfd_residual_code_division_bounded_execution = ff_q_pfp_division_bounded_executiontrimremovedentry * S ((S (pfp_repeat_index_division_bounded_executiontrimremoved)) * pfd_residual_scale_division_bounded_execution) + (0)))) /\ (((forall pftrim_index_division_bounded_executiontrimsuffix pftrim_value_division_bounded_executiontrimsuffix. (exists pfa_gap_division_bounded_executiontrimsuffixbound. pfa_gap_division_bounded_executiontrimsuffixbound + S (pftrim_index_division_bounded_executiontrimsuffix) = (R)) -> (((exists ff_h_pfp_division_bounded_executiontrimsuffixsource. ff_h_pfp_division_bounded_executiontrimsuffixsource + S (pftrim_value_division_bounded_executiontrimsuffix) = S ((S ((pfd_cut_division_bounded_execution)+pftrim_index_division_bounded_executiontrimsuffix)) * pfd_residual_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executiontrimsuffixsource. pfd_residual_code_division_bounded_execution = ff_q_pfp_division_bounded_executiontrimsuffixsource * S ((S ((pfd_cut_division_bounded_execution)+pftrim_index_division_bounded_executiontrimsuffix)) * pfd_residual_scale_division_bounded_execution) + (pftrim_value_division_bounded_executiontrimsuffix))) -> (((exists ff_h_pfp_division_bounded_executiontrimsuffixoutput. ff_h_pfp_division_bounded_executiontrimsuffixoutput + S (pftrim_value_division_bounded_executiontrimsuffix) = S ((S (pftrim_index_division_bounded_executiontrimsuffix)) * rc)) /\ exists ff_q_pfp_division_bounded_executiontrimsuffixoutput. rb = ff_q_pfp_division_bounded_executiontrimsuffixoutput * S ((S (pftrim_index_division_bounded_executiontrimsuffix)) * rc) + (pftrim_value_division_bounded_executiontrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_bounded_executiontrimnormal. ((((exists ff_h_pfp_division_bounded_executiontrimnormalentry. ff_h_pfp_division_bounded_executiontrimnormalentry + S (pftrim_leading_division_bounded_executiontrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_bounded_executiontrimnormalentry. rb = ff_q_pfp_division_bounded_executiontrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_bounded_executiontrimnormal))) /\ ((~(pftrim_leading_division_bounded_executiontrimnormal=0))))))))))))))))))))))))))))))))) /\ (((R)=0 \/ (exists pfd_remainder_degree_division_bounded_degree. (((((R)=S (pfd_remainder_degree_division_bounded_degree)) /\ (((forall fom_index_pfp_division_bounded_degreerepresentedcoefficients. (exists fom_gap_pfp_division_bounded_degreerepresentedcoefficients_index_bound. fom_gap_pfp_division_bounded_degreerepresentedcoefficients_index_bound + S (fom_index_pfp_division_bounded_degreerepresentedcoefficients) = R) -> exists fom_value_pfp_division_bounded_degreerepresentedcoefficients. ((((exists fom_beta_height_pfp_division_bounded_degreerepresentedcoefficients_entry. fom_beta_height_pfp_division_bounded_degreerepresentedcoefficients_entry + S (fom_value_pfp_division_bounded_degreerepresentedcoefficients) = S ((S (fom_index_pfp_division_bounded_degreerepresentedcoefficients)) * rc)) /\ exists fom_beta_quotient_pfp_division_bounded_degreerepresentedcoefficients_entry. rb = fom_beta_quotient_pfp_division_bounded_degreerepresentedcoefficients_entry * S ((S (fom_index_pfp_division_bounded_degreerepresentedcoefficients)) * rc) + (fom_value_pfp_division_bounded_degreerepresentedcoefficients))) /\ (exists fom_gap_pfp_division_bounded_degreerepresentedcoefficients_value_bound. fom_gap_pfp_division_bounded_degreerepresentedcoefficients_value_bound + S (fom_value_pfp_division_bounded_degreerepresentedcoefficients) = p))) /\ ((exists pfd_leading_division_bounded_degreerepresented. ((((exists ff_h_pfp_division_bounded_degreerepresentedentry. ff_h_pfp_division_bounded_degreerepresentedentry + S (pfd_leading_division_bounded_degreerepresented) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_bounded_degreerepresentedentry. rb = ff_q_pfp_division_bounded_degreerepresentedentry * S ((S (0)) * rc) + (pfd_leading_division_bounded_degreerepresented))) /\ ((~(pfd_leading_division_bounded_degreerepresented=0)))))))))) /\ ((exists pfa_gap_division_bounded_degreestrict. pfa_gap_division_bounded_degreestrict + S (pfd_remainder_degree_division_bounded_degree) = (d))))))))

Constructive proof overview

Generated structural guide

Unconditionally construct an actual general division execution and derive its strict remainder-degree alternative; no theorem claims degree for zero.

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

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

Proof neighborhood

Direct dependencies

PX0039 prime_field_polynomial_division_execution_exists PX003A prime_field_polynomial_division_remainder_degree

Direct dependents

none

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

52 script commands · 8 reading checkpoints · 1 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 execution existsprime field polynomial division remainder degree

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 hL11–20

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

  1. L11
    have h : ∃ qb. ∃ qc. ∃ q. ∃ rb. ∃ rc. ∃ R. FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R)Definitions: FpPolynomialDivisionExecution
  2. L12
    specialize prime_field_polynomial_division_execution_exists (p)
  3. L13
    specialize prime_field_polynomial_division_execution_exists (ab)
  4. L14
    specialize prime_field_polynomial_division_execution_exists (ac)
  5. L15
    specialize prime_field_polynomial_division_execution_exists (L)
  6. L16
    specialize prime_field_polynomial_division_execution_exists (bb)
  7. L17
    specialize prime_field_polynomial_division_execution_exists (bc)
  8. L18
    specialize prime_field_polynomial_division_execution_exists (d)
  9. L19
    apply prime_field_polynomial_division_execution_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–28

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

  1. L23
    cases h
  2. L24
    cases h_witness
  3. L25
    cases h_witness_witness
  4. L26
    cases h_witness_witness_witness
  5. L27
    cases h_witness_witness_witness_witness
  6. L28
    cases h_witness_witness_witness_witness_witness
05Construct an explicit witnessL29–34

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

  1. L29
    exists x
  2. L30
    exists x1
  3. L31
    exists x2
  4. L32
    exists x3
  5. L33
    exists x4
  6. L34
    exists x5
06Separate the logical casesL35–35

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

  1. L35
    split
07Use earlier factsL36–45

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

  1. L36
    exact h_witness_witness_witness_witness_witness_witness
  2. L37
    specialize prime_field_polynomial_division_remainder_degree (p)
  3. L38
    specialize prime_field_polynomial_division_remainder_degree (ab)
  4. L39
    specialize prime_field_polynomial_division_remainder_degree (ac)
  5. L40
    specialize prime_field_polynomial_division_remainder_degree (L)
  6. L41
    specialize prime_field_polynomial_division_remainder_degree (bb)
  7. L42
    specialize prime_field_polynomial_division_remainder_degree (bc)
  8. L43
    specialize prime_field_polynomial_division_remainder_degree (d)
  9. L44
    specialize prime_field_polynomial_division_remainder_degree (x)
  10. L45
    specialize prime_field_polynomial_division_remainder_degree (x1)
08Use earlier factsL46–52

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

  1. L46
    specialize prime_field_polynomial_division_remainder_degree (x2)
  2. L47
    specialize prime_field_polynomial_division_remainder_degree (x3)
  3. L48
    specialize prime_field_polynomial_division_remainder_degree (x4)
  4. L49
    specialize prime_field_polynomial_division_remainder_degree (x5)
  5. L50
    apply prime_field_polynomial_division_remainder_degree
  6. L51
    exact hp
  7. L52
    exact h_witness_witness_witness_witness_witness_witness

Library-wide reading audit

Original exact command ledger · 52 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 h : exists qb qc q rb rc R. (((forall fom_index_pfp_division_bounded_choseninput. (exists fom_gap_pfp_division_bounded_choseninput_index_bound. fom_gap_pfp_division_bounded_choseninput_index_bound + S (fom_index_pfp_division_bounded_choseninput) = L) -> exists fom_value_pfp_division_bounded_choseninput. ((((exists fom_beta_height_pfp_division_bounded_choseninput_entry. fom_beta_height_pfp_division_bounded_choseninput_entry + S (fom_value_pfp_division_bounded_choseninput) = S ((S (fom_index_pfp_division_bounded_choseninput)) * ac)) /\ exists fom_beta_quotient_pfp_division_bounded_choseninput_entry. ab = fom_beta_quotient_pfp_division_bounded_choseninput_entry * S ((S (fom_index_pfp_division_bounded_choseninput)) * ac) + (fom_value_pfp_division_bounded_choseninput))) /\ (exists fom_gap_pfp_division_bounded_choseninput_value_bound. fom_gap_pfp_division_bounded_choseninput_value_bound + S (fom_value_pfp_division_bounded_choseninput) = p))) /\ (((forall fom_index_pfp_division_bounded_chosendivisor. (exists fom_gap_pfp_division_bounded_chosendivisor_index_bound. fom_gap_pfp_division_bounded_chosendivisor_index_bound + S (fom_index_pfp_division_bounded_chosendivisor) = S (d)) -> exists fom_value_pfp_division_bounded_chosendivisor. ((((exists fom_beta_height_pfp_division_bounded_chosendivisor_entry. fom_beta_height_pfp_division_bounded_chosendivisor_entry + S (fom_value_pfp_division_bounded_chosendivisor) = S ((S (fom_index_pfp_division_bounded_chosendivisor)) * bc)) /\ exists fom_beta_quotient_pfp_division_bounded_chosendivisor_entry. bb = fom_beta_quotient_pfp_division_bounded_chosendivisor_entry * S ((S (fom_index_pfp_division_bounded_chosendivisor)) * bc) + (fom_value_pfp_division_bounded_chosendivisor))) /\ (exists fom_gap_pfp_division_bounded_chosendivisor_value_bound. fom_gap_pfp_division_bounded_chosendivisor_value_bound + S (fom_value_pfp_division_bounded_chosendivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_division_bounded_chosenlengthshort. pfc_gap_division_bounded_chosenlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_division_bounded_chosen pfd_inverse_division_bounded_chosen pfd_product_code_division_bounded_chosen pfd_product_scale_division_bounded_chosen pfd_residual_code_division_bounded_chosen pfd_residual_scale_division_bounded_chosen pfd_cut_division_bounded_chosen. ((((exists ff_h_pfp_division_bounded_chosenhead. ff_h_pfp_division_bounded_chosenhead + S (pfd_head_division_bounded_chosen) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_bounded_chosenhead. bb = ff_q_pfp_division_bounded_chosenhead * S ((S (0)) * bc) + (pfd_head_division_bounded_chosen))) /\ (((((~((pfd_head_division_bounded_chosen) = 0)) /\ ((((exists pfa_gap_division_bounded_choseninversemultiplicationleft. pfa_gap_division_bounded_choseninversemultiplicationleft + S (pfd_head_division_bounded_chosen) = (p)) /\ (((exists pfa_gap_division_bounded_choseninversemultiplicationright. pfa_gap_division_bounded_choseninversemultiplicationright + S (pfd_inverse_division_bounded_chosen) = (p)) /\ ((((exists pfa_gap_division_bounded_choseninversemultiplicationresultbound. pfa_gap_division_bounded_choseninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_bounded_choseninversemultiplicationresultcongruence pfa_offset_right_division_bounded_choseninversemultiplicationresultcongruence. ((pfd_head_division_bounded_chosen) * (pfd_inverse_division_bounded_chosen)) + (p) * pfa_offset_left_division_bounded_choseninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_bounded_choseninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_division_bounded_chosenquotient. (exists pfa_gap_division_bounded_chosenquotientbound. pfa_gap_division_bounded_chosenquotientbound + S (pfd_index_division_bounded_chosenquotient) = (q)) -> exists pfd_value_division_bounded_chosenquotient. ((((exists ff_h_pfp_division_bounded_chosenquotiententry. ff_h_pfp_division_bounded_chosenquotiententry + S (pfd_value_division_bounded_chosenquotient) = S ((S (pfd_index_division_bounded_chosenquotient)) * qc)) /\ exists ff_q_pfp_division_bounded_chosenquotiententry. qb = ff_q_pfp_division_bounded_chosenquotiententry * S ((S (pfd_index_division_bounded_chosenquotient)) * qc) + (pfd_value_division_bounded_chosenquotient))) /\ ((exists pfd_input_division_bounded_chosenquotientstep pfd_previous_division_bounded_chosenquotientstep pfd_difference_division_bounded_chosenquotientstep. ((((exists ff_h_pfp_division_bounded_chosenquotientstepinput. ff_h_pfp_division_bounded_chosenquotientstepinput + S (pfd_input_division_bounded_chosenquotientstep) = S ((S (pfd_index_division_bounded_chosenquotient)) * ac)) /\ exists ff_q_pfp_division_bounded_chosenquotientstepinput. ab = ff_q_pfp_division_bounded_chosenquotientstepinput * S ((S (pfd_index_division_bounded_chosenquotient)) * ac) + (pfd_input_division_bounded_chosenquotientstep))) /\ (((exists pfc_terms_code_division_bounded_chosenquotientstepprevious pfc_terms_scale_division_bounded_chosenquotientstepprevious pfc_natural_sum_division_bounded_chosenquotientstepprevious. ((forall pfc_index_division_bounded_chosenquotientsteppreviousdiagonal. (exists pfa_gap_division_bounded_chosenquotientsteppreviousdiagonalbound. pfa_gap_division_bounded_chosenquotientsteppreviousdiagonalbound + S (pfc_index_division_bounded_chosenquotientsteppreviousdiagonal) = (S (pfd_index_division_bounded_chosenquotient))) -> exists pfc_value_division_bounded_chosenquotientsteppreviousdiagonal. ((((exists ff_h_pfp_division_bounded_chosenquotientsteppreviousdiagonalentry. ff_h_pfp_division_bounded_chosenquotientsteppreviousdiagonalentry + S (pfc_value_division_bounded_chosenquotientsteppreviousdiagonal) = S ((S (pfc_index_division_bounded_chosenquotientsteppreviousdiagonal)) * pfc_terms_scale_division_bounded_chosenquotientstepprevious)) /\ exists ff_q_pfp_division_bounded_chosenquotientsteppreviousdiagonalentry. pfc_terms_code_division_bounded_chosenquotientstepprevious = ff_q_pfp_division_bounded_chosenquotientsteppreviousdiagonalentry * S ((S (pfc_index_division_bounded_chosenquotientsteppreviousdiagonal)) * pfc_terms_scale_division_bounded_chosenquotientstepprevious) + (pfc_value_division_bounded_chosenquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_division_bounded_chosenquotientsteppreviousdiagonalterm pfc_left_division_bounded_chosenquotientsteppreviousdiagonalterm pfc_right_division_bounded_chosenquotientsteppreviousdiagonalterm. (((pfc_index_division_bounded_chosenquotientsteppreviousdiagonal)+pfc_complement_division_bounded_chosenquotientsteppreviousdiagonalterm=(pfd_index_division_bounded_chosenquotient)) /\ ((((((exists pfa_gap_division_bounded_chosenquotientsteppreviousdiagonaltermleftinside. pfa_gap_division_bounded_chosenquotientsteppreviousdiagonaltermleftinside + S (pfc_index_division_bounded_chosenquotientsteppreviousdiagonal) = (pfd_index_division_bounded_chosenquotient)) /\ ((((exists ff_h_pfp_division_bounded_chosenquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_division_bounded_chosenquotientsteppreviousdiagonaltermleftentry + S (pfc_left_division_bounded_chosenquotientsteppreviousdiagonalterm) = S ((S (pfc_index_division_bounded_chosenquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_bounded_chosenquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_bounded_chosenquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_bounded_chosenquotientsteppreviousdiagonal)) * qc) + (pfc_left_division_bounded_chosenquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_chosenquotientsteppreviousdiagonaltermleftoutside. pfc_gap_division_bounded_chosenquotientsteppreviousdiagonaltermleftoutside+(pfd_index_division_bounded_chosenquotient)=(pfc_index_division_bounded_chosenquotientsteppreviousdiagonal)) /\ (((pfc_left_division_bounded_chosenquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_bounded_chosenquotientsteppreviousdiagonaltermrightinside. pfa_gap_division_bounded_chosenquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_division_bounded_chosenquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_bounded_chosenquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_division_bounded_chosenquotientsteppreviousdiagonaltermrightentry + S (pfc_right_division_bounded_chosenquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_division_bounded_chosenquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_bounded_chosenquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_bounded_chosenquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_bounded_chosenquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_division_bounded_chosenquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_chosenquotientsteppreviousdiagonaltermrightoutside. pfc_gap_division_bounded_chosenquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_division_bounded_chosenquotientsteppreviousdiagonalterm)) /\ (((pfc_right_division_bounded_chosenquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_bounded_chosenquotientsteppreviousdiagonal)=pfc_left_division_bounded_chosenquotientsteppreviousdiagonalterm*pfc_right_division_bounded_chosenquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_bounded_chosenquotientstepprevioussum fs_v_pfc_division_bounded_chosenquotientstepprevioussum. ((((exists fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_start. fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_bounded_chosenquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_start. fs_u_pfc_division_bounded_chosenquotientstepprevioussum = fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_bounded_chosenquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_terminal. fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_terminal + S (pfc_natural_sum_division_bounded_chosenquotientstepprevious) = S ((S (S (pfd_index_division_bounded_chosenquotient))) * fs_v_pfc_division_bounded_chosenquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_terminal. fs_u_pfc_division_bounded_chosenquotientstepprevioussum = fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_division_bounded_chosenquotient))) * fs_v_pfc_division_bounded_chosenquotientstepprevioussum) + (pfc_natural_sum_division_bounded_chosenquotientstepprevious))) /\ forall fs_i_pfc_division_bounded_chosenquotientstepprevioussum_body_steps. (exists fs_lt_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_bound. fs_lt_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_bound + S fs_i_pfc_division_bounded_chosenquotientstepprevioussum_body_steps = S (pfd_index_division_bounded_chosenquotient)) -> exists fs_a_pfc_division_bounded_chosenquotientstepprevioussum_body_steps fs_r_pfc_division_bounded_chosenquotientstepprevioussum_body_steps fs_s_pfc_division_bounded_chosenquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_summand. fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_division_bounded_chosenquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_bounded_chosenquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_bounded_chosenquotientstepprevious)) /\ exists fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_summand. pfc_terms_code_division_bounded_chosenquotientstepprevious = fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_bounded_chosenquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_bounded_chosenquotientstepprevious) + (fs_a_pfc_division_bounded_chosenquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_partial. fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_division_bounded_chosenquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_bounded_chosenquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_chosenquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_partial. fs_u_pfc_division_bounded_chosenquotientstepprevioussum = fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_bounded_chosenquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_chosenquotientstepprevioussum) + (fs_r_pfc_division_bounded_chosenquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_successor. fs_h_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_division_bounded_chosenquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_bounded_chosenquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_chosenquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_successor. fs_u_pfc_division_bounded_chosenquotientstepprevioussum = fs_q_pfc_division_bounded_chosenquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_bounded_chosenquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_chosenquotientstepprevioussum) + (fs_s_pfc_division_bounded_chosenquotientstepprevioussum_body_steps))) /\ fs_s_pfc_division_bounded_chosenquotientstepprevioussum_body_steps = fs_r_pfc_division_bounded_chosenquotientstepprevioussum_body_steps + fs_a_pfc_division_bounded_chosenquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_bounded_chosenquotientsteppreviousresiduebound. pfa_gap_division_bounded_chosenquotientsteppreviousresiduebound + S (pfd_previous_division_bounded_chosenquotientstep) = (p)) /\ ((exists pfa_offset_left_division_bounded_chosenquotientsteppreviousresiduecongruence pfa_offset_right_division_bounded_chosenquotientsteppreviousresiduecongruence. (pfc_natural_sum_division_bounded_chosenquotientstepprevious) + (p) * pfa_offset_left_division_bounded_chosenquotientsteppreviousresiduecongruence = (pfd_previous_division_bounded_chosenquotientstep) + (p) * pfa_offset_right_division_bounded_chosenquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_bounded_chosenquotientstepsubtractleft. pfa_gap_division_bounded_chosenquotientstepsubtractleft + S (pfd_previous_division_bounded_chosenquotientstep) = (p)) /\ (((exists pfa_gap_division_bounded_chosenquotientstepsubtractright. pfa_gap_division_bounded_chosenquotientstepsubtractright + S (pfd_difference_division_bounded_chosenquotientstep) = (p)) /\ ((((exists pfa_gap_division_bounded_chosenquotientstepsubtractresultbound. pfa_gap_division_bounded_chosenquotientstepsubtractresultbound + S (pfd_input_division_bounded_chosenquotientstep) = (p)) /\ ((exists pfa_offset_left_division_bounded_chosenquotientstepsubtractresultcongruence pfa_offset_right_division_bounded_chosenquotientstepsubtractresultcongruence. ((pfd_previous_division_bounded_chosenquotientstep) + (pfd_difference_division_bounded_chosenquotientstep)) + (p) * pfa_offset_left_division_bounded_chosenquotientstepsubtractresultcongruence = (pfd_input_division_bounded_chosenquotientstep) + (p) * pfa_offset_right_division_bounded_chosenquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_bounded_chosenquotientstepmultiplyleft. pfa_gap_division_bounded_chosenquotientstepmultiplyleft + S (pfd_inverse_division_bounded_chosen) = (p)) /\ (((exists pfa_gap_division_bounded_chosenquotientstepmultiplyright. pfa_gap_division_bounded_chosenquotientstepmultiplyright + S (pfd_difference_division_bounded_chosenquotientstep) = (p)) /\ ((((exists pfa_gap_division_bounded_chosenquotientstepmultiplyresultbound. pfa_gap_division_bounded_chosenquotientstepmultiplyresultbound + S (pfd_value_division_bounded_chosenquotient) = (p)) /\ ((exists pfa_offset_left_division_bounded_chosenquotientstepmultiplyresultcongruence pfa_offset_right_division_bounded_chosenquotientstepmultiplyresultcongruence. ((pfd_inverse_division_bounded_chosen) * (pfd_difference_division_bounded_chosenquotientstep)) + (p) * pfa_offset_left_division_bounded_chosenquotientstepmultiplyresultcongruence = (pfd_value_division_bounded_chosenquotient) + (p) * pfa_offset_right_division_bounded_chosenquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_division_bounded_chosenproduct. (exists pfa_gap_division_bounded_chosenproductbound. pfa_gap_division_bounded_chosenproductbound + S (pfc_index_division_bounded_chosenproduct) = (L)) -> exists pfc_value_division_bounded_chosenproduct. ((((exists ff_h_pfp_division_bounded_chosenproductentry. ff_h_pfp_division_bounded_chosenproductentry + S (pfc_value_division_bounded_chosenproduct) = S ((S (pfc_index_division_bounded_chosenproduct)) * pfd_product_scale_division_bounded_chosen)) /\ exists ff_q_pfp_division_bounded_chosenproductentry. pfd_product_code_division_bounded_chosen = ff_q_pfp_division_bounded_chosenproductentry * S ((S (pfc_index_division_bounded_chosenproduct)) * pfd_product_scale_division_bounded_chosen) + (pfc_value_division_bounded_chosenproduct))) /\ ((exists pfc_terms_code_division_bounded_chosenproductcoefficient pfc_terms_scale_division_bounded_chosenproductcoefficient pfc_natural_sum_division_bounded_chosenproductcoefficient. ((forall pfc_index_division_bounded_chosenproductcoefficientdiagonal. (exists pfa_gap_division_bounded_chosenproductcoefficientdiagonalbound. pfa_gap_division_bounded_chosenproductcoefficientdiagonalbound + S (pfc_index_division_bounded_chosenproductcoefficientdiagonal) = (S (pfc_index_division_bounded_chosenproduct))) -> exists pfc_value_division_bounded_chosenproductcoefficientdiagonal. ((((exists ff_h_pfp_division_bounded_chosenproductcoefficientdiagonalentry. ff_h_pfp_division_bounded_chosenproductcoefficientdiagonalentry + S (pfc_value_division_bounded_chosenproductcoefficientdiagonal) = S ((S (pfc_index_division_bounded_chosenproductcoefficientdiagonal)) * pfc_terms_scale_division_bounded_chosenproductcoefficient)) /\ exists ff_q_pfp_division_bounded_chosenproductcoefficientdiagonalentry. pfc_terms_code_division_bounded_chosenproductcoefficient = ff_q_pfp_division_bounded_chosenproductcoefficientdiagonalentry * S ((S (pfc_index_division_bounded_chosenproductcoefficientdiagonal)) * pfc_terms_scale_division_bounded_chosenproductcoefficient) + (pfc_value_division_bounded_chosenproductcoefficientdiagonal))) /\ ((exists pfc_complement_division_bounded_chosenproductcoefficientdiagonalterm pfc_left_division_bounded_chosenproductcoefficientdiagonalterm pfc_right_division_bounded_chosenproductcoefficientdiagonalterm. (((pfc_index_division_bounded_chosenproductcoefficientdiagonal)+pfc_complement_division_bounded_chosenproductcoefficientdiagonalterm=(pfc_index_division_bounded_chosenproduct)) /\ ((((((exists pfa_gap_division_bounded_chosenproductcoefficientdiagonaltermleftinside. pfa_gap_division_bounded_chosenproductcoefficientdiagonaltermleftinside + S (pfc_index_division_bounded_chosenproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_bounded_chosenproductcoefficientdiagonaltermleftentry. ff_h_pfp_division_bounded_chosenproductcoefficientdiagonaltermleftentry + S (pfc_left_division_bounded_chosenproductcoefficientdiagonalterm) = S ((S (pfc_index_division_bounded_chosenproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_bounded_chosenproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_bounded_chosenproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_bounded_chosenproductcoefficientdiagonal)) * qc) + (pfc_left_division_bounded_chosenproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_chosenproductcoefficientdiagonaltermleftoutside. pfc_gap_division_bounded_chosenproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_bounded_chosenproductcoefficientdiagonal)) /\ (((pfc_left_division_bounded_chosenproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_bounded_chosenproductcoefficientdiagonaltermrightinside. pfa_gap_division_bounded_chosenproductcoefficientdiagonaltermrightinside + S (pfc_complement_division_bounded_chosenproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_bounded_chosenproductcoefficientdiagonaltermrightentry. ff_h_pfp_division_bounded_chosenproductcoefficientdiagonaltermrightentry + S (pfc_right_division_bounded_chosenproductcoefficientdiagonalterm) = S ((S (pfc_complement_division_bounded_chosenproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_bounded_chosenproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_bounded_chosenproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_bounded_chosenproductcoefficientdiagonalterm)) * bc) + (pfc_right_division_bounded_chosenproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_chosenproductcoefficientdiagonaltermrightoutside. pfc_gap_division_bounded_chosenproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_bounded_chosenproductcoefficientdiagonalterm)) /\ (((pfc_right_division_bounded_chosenproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_bounded_chosenproductcoefficientdiagonal)=pfc_left_division_bounded_chosenproductcoefficientdiagonalterm*pfc_right_division_bounded_chosenproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_bounded_chosenproductcoefficientsum fs_v_pfc_division_bounded_chosenproductcoefficientsum. ((((exists fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_start. fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_bounded_chosenproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_start. fs_u_pfc_division_bounded_chosenproductcoefficientsum = fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_bounded_chosenproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_terminal. fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_terminal + S (pfc_natural_sum_division_bounded_chosenproductcoefficient) = S ((S (S (pfc_index_division_bounded_chosenproduct))) * fs_v_pfc_division_bounded_chosenproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_terminal. fs_u_pfc_division_bounded_chosenproductcoefficientsum = fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_terminal * S ((S (S (pfc_index_division_bounded_chosenproduct))) * fs_v_pfc_division_bounded_chosenproductcoefficientsum) + (pfc_natural_sum_division_bounded_chosenproductcoefficient))) /\ forall fs_i_pfc_division_bounded_chosenproductcoefficientsum_body_steps. (exists fs_lt_pfc_division_bounded_chosenproductcoefficientsum_body_steps_bound. fs_lt_pfc_division_bounded_chosenproductcoefficientsum_body_steps_bound + S fs_i_pfc_division_bounded_chosenproductcoefficientsum_body_steps = S (pfc_index_division_bounded_chosenproduct)) -> exists fs_a_pfc_division_bounded_chosenproductcoefficientsum_body_steps fs_r_pfc_division_bounded_chosenproductcoefficientsum_body_steps fs_s_pfc_division_bounded_chosenproductcoefficientsum_body_steps. ((((exists fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_steps_summand. fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_steps_summand + S (fs_a_pfc_division_bounded_chosenproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_bounded_chosenproductcoefficientsum_body_steps)) * pfc_terms_scale_division_bounded_chosenproductcoefficient)) /\ exists fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_steps_summand. pfc_terms_code_division_bounded_chosenproductcoefficient = fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_bounded_chosenproductcoefficientsum_body_steps)) * pfc_terms_scale_division_bounded_chosenproductcoefficient) + (fs_a_pfc_division_bounded_chosenproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_steps_partial. fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_steps_partial + S (fs_r_pfc_division_bounded_chosenproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_bounded_chosenproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_chosenproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_steps_partial. fs_u_pfc_division_bounded_chosenproductcoefficientsum = fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_bounded_chosenproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_chosenproductcoefficientsum) + (fs_r_pfc_division_bounded_chosenproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_steps_successor. fs_h_pfc_division_bounded_chosenproductcoefficientsum_body_steps_successor + S (fs_s_pfc_division_bounded_chosenproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_bounded_chosenproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_chosenproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_steps_successor. fs_u_pfc_division_bounded_chosenproductcoefficientsum = fs_q_pfc_division_bounded_chosenproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_bounded_chosenproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_chosenproductcoefficientsum) + (fs_s_pfc_division_bounded_chosenproductcoefficientsum_body_steps))) /\ fs_s_pfc_division_bounded_chosenproductcoefficientsum_body_steps = fs_r_pfc_division_bounded_chosenproductcoefficientsum_body_steps + fs_a_pfc_division_bounded_chosenproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_bounded_chosenproductcoefficientresiduebound. pfa_gap_division_bounded_chosenproductcoefficientresiduebound + S (pfc_value_division_bounded_chosenproduct) = (p)) /\ ((exists pfa_offset_left_division_bounded_chosenproductcoefficientresiduecongruence pfa_offset_right_division_bounded_chosenproductcoefficientresiduecongruence. (pfc_natural_sum_division_bounded_chosenproductcoefficient) + (p) * pfa_offset_left_division_bounded_chosenproductcoefficientresiduecongruence = (pfc_value_division_bounded_chosenproduct) + (p) * pfa_offset_right_division_bounded_chosenproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_division_bounded_chosendifference. (exists pfa_gap_division_bounded_chosendifferenceindex. pfa_gap_division_bounded_chosendifferenceindex + S (pfs_index_division_bounded_chosendifference) = (L)) -> exists pfs_left_division_bounded_chosendifference pfs_right_division_bounded_chosendifference pfs_result_division_bounded_chosendifference. ((((exists ff_h_pfp_division_bounded_chosendifferenceleft. ff_h_pfp_division_bounded_chosendifferenceleft + S (pfs_left_division_bounded_chosendifference) = S ((S (pfs_index_division_bounded_chosendifference)) * ac)) /\ exists ff_q_pfp_division_bounded_chosendifferenceleft. ab = ff_q_pfp_division_bounded_chosendifferenceleft * S ((S (pfs_index_division_bounded_chosendifference)) * ac) + (pfs_left_division_bounded_chosendifference))) /\ (((((exists ff_h_pfp_division_bounded_chosendifferenceright. ff_h_pfp_division_bounded_chosendifferenceright + S (pfs_right_division_bounded_chosendifference) = S ((S (pfs_index_division_bounded_chosendifference)) * pfd_product_scale_division_bounded_chosen)) /\ exists ff_q_pfp_division_bounded_chosendifferenceright. pfd_product_code_division_bounded_chosen = ff_q_pfp_division_bounded_chosendifferenceright * S ((S (pfs_index_division_bounded_chosendifference)) * pfd_product_scale_division_bounded_chosen) + (pfs_right_division_bounded_chosendifference))) /\ (((((exists ff_h_pfp_division_bounded_chosendifferenceresult. ff_h_pfp_division_bounded_chosendifferenceresult + S (pfs_result_division_bounded_chosendifference) = S ((S (pfs_index_division_bounded_chosendifference)) * pfd_residual_scale_division_bounded_chosen)) /\ exists ff_q_pfp_division_bounded_chosendifferenceresult. pfd_residual_code_division_bounded_chosen = ff_q_pfp_division_bounded_chosendifferenceresult * S ((S (pfs_index_division_bounded_chosendifference)) * pfd_residual_scale_division_bounded_chosen) + (pfs_result_division_bounded_chosendifference))) /\ ((((exists pfa_gap_division_bounded_chosendifferenceoperationleft. pfa_gap_division_bounded_chosendifferenceoperationleft + S (pfs_right_division_bounded_chosendifference) = (p)) /\ (((exists pfa_gap_division_bounded_chosendifferenceoperationright. pfa_gap_division_bounded_chosendifferenceoperationright + S (pfs_result_division_bounded_chosendifference) = (p)) /\ ((((exists pfa_gap_division_bounded_chosendifferenceoperationresultbound. pfa_gap_division_bounded_chosendifferenceoperationresultbound + S (pfs_left_division_bounded_chosendifference) = (p)) /\ ((exists pfa_offset_left_division_bounded_chosendifferenceoperationresultcongruence pfa_offset_right_division_bounded_chosendifferenceoperationresultcongruence. ((pfs_right_division_bounded_chosendifference) + (pfs_result_division_bounded_chosendifference)) + (p) * pfa_offset_left_division_bounded_chosendifferenceoperationresultcongruence = (pfs_left_division_bounded_chosendifference) + (p) * pfa_offset_right_division_bounded_chosendifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_division_bounded_chosen)+(R)) /\ (((forall fom_index_pfp_division_bounded_chosentriminput. (exists fom_gap_pfp_division_bounded_chosentriminput_index_bound. fom_gap_pfp_division_bounded_chosentriminput_index_bound + S (fom_index_pfp_division_bounded_chosentriminput) = L) -> exists fom_value_pfp_division_bounded_chosentriminput. ((((exists fom_beta_height_pfp_division_bounded_chosentriminput_entry. fom_beta_height_pfp_division_bounded_chosentriminput_entry + S (fom_value_pfp_division_bounded_chosentriminput) = S ((S (fom_index_pfp_division_bounded_chosentriminput)) * pfd_residual_scale_division_bounded_chosen)) /\ exists fom_beta_quotient_pfp_division_bounded_chosentriminput_entry. pfd_residual_code_division_bounded_chosen = fom_beta_quotient_pfp_division_bounded_chosentriminput_entry * S ((S (fom_index_pfp_division_bounded_chosentriminput)) * pfd_residual_scale_division_bounded_chosen) + (fom_value_pfp_division_bounded_chosentriminput))) /\ (exists fom_gap_pfp_division_bounded_chosentriminput_value_bound. fom_gap_pfp_division_bounded_chosentriminput_value_bound + S (fom_value_pfp_division_bounded_chosentriminput) = p))) /\ (((forall pfp_repeat_index_division_bounded_chosentrimremoved. (exists pfa_gap_division_bounded_chosentrimremovedindex. pfa_gap_division_bounded_chosentrimremovedindex + S (pfp_repeat_index_division_bounded_chosentrimremoved) = (pfd_cut_division_bounded_chosen)) -> (((exists ff_h_pfp_division_bounded_chosentrimremovedentry. ff_h_pfp_division_bounded_chosentrimremovedentry + S (0) = S ((S (pfp_repeat_index_division_bounded_chosentrimremoved)) * pfd_residual_scale_division_bounded_chosen)) /\ exists ff_q_pfp_division_bounded_chosentrimremovedentry. pfd_residual_code_division_bounded_chosen = ff_q_pfp_division_bounded_chosentrimremovedentry * S ((S (pfp_repeat_index_division_bounded_chosentrimremoved)) * pfd_residual_scale_division_bounded_chosen) + (0)))) /\ (((forall pftrim_index_division_bounded_chosentrimsuffix pftrim_value_division_bounded_chosentrimsuffix. (exists pfa_gap_division_bounded_chosentrimsuffixbound. pfa_gap_division_bounded_chosentrimsuffixbound + S (pftrim_index_division_bounded_chosentrimsuffix) = (R)) -> (((exists ff_h_pfp_division_bounded_chosentrimsuffixsource. ff_h_pfp_division_bounded_chosentrimsuffixsource + S (pftrim_value_division_bounded_chosentrimsuffix) = S ((S ((pfd_cut_division_bounded_chosen)+pftrim_index_division_bounded_chosentrimsuffix)) * pfd_residual_scale_division_bounded_chosen)) /\ exists ff_q_pfp_division_bounded_chosentrimsuffixsource. pfd_residual_code_division_bounded_chosen = ff_q_pfp_division_bounded_chosentrimsuffixsource * S ((S ((pfd_cut_division_bounded_chosen)+pftrim_index_division_bounded_chosentrimsuffix)) * pfd_residual_scale_division_bounded_chosen) + (pftrim_value_division_bounded_chosentrimsuffix))) -> (((exists ff_h_pfp_division_bounded_chosentrimsuffixoutput. ff_h_pfp_division_bounded_chosentrimsuffixoutput + S (pftrim_value_division_bounded_chosentrimsuffix) = S ((S (pftrim_index_division_bounded_chosentrimsuffix)) * rc)) /\ exists ff_q_pfp_division_bounded_chosentrimsuffixoutput. rb = ff_q_pfp_division_bounded_chosentrimsuffixoutput * S ((S (pftrim_index_division_bounded_chosentrimsuffix)) * rc) + (pftrim_value_division_bounded_chosentrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_bounded_chosentrimnormal. ((((exists ff_h_pfp_division_bounded_chosentrimnormalentry. ff_h_pfp_division_bounded_chosentrimnormalentry + S (pftrim_leading_division_bounded_chosentrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_bounded_chosentrimnormalentry. rb = ff_q_pfp_division_bounded_chosentrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_bounded_chosentrimnormal))) /\ ((~(pftrim_leading_division_bounded_chosentrimnormal=0)))))))))))))))))))))))))))))))))
  12. 0012specialize prime_field_polynomial_division_execution_exists (p)
  13. 0013specialize prime_field_polynomial_division_execution_exists (ab)
  14. 0014specialize prime_field_polynomial_division_execution_exists (ac)
  15. 0015specialize prime_field_polynomial_division_execution_exists (L)
  16. 0016specialize prime_field_polynomial_division_execution_exists (bb)
  17. 0017specialize prime_field_polynomial_division_execution_exists (bc)
  18. 0018specialize prime_field_polynomial_division_execution_exists (d)
  19. 0019apply prime_field_polynomial_division_execution_exists
  20. 0020exact hp
  21. 0021exact ha
  22. 0022exact hb
  23. 0023cases h
  24. 0024cases h_witness
  25. 0025cases h_witness_witness
  26. 0026cases h_witness_witness_witness
  27. 0027cases h_witness_witness_witness_witness
  28. 0028cases h_witness_witness_witness_witness_witness
  29. 0029exists x
  30. 0030exists x1
  31. 0031exists x2
  32. 0032exists x3
  33. 0033exists x4
  34. 0034exists x5
  35. 0035split
  36. 0036exact h_witness_witness_witness_witness_witness_witness
  37. 0037specialize prime_field_polynomial_division_remainder_degree (p)
  38. 0038specialize prime_field_polynomial_division_remainder_degree (ab)
  39. 0039specialize prime_field_polynomial_division_remainder_degree (ac)
  40. 0040specialize prime_field_polynomial_division_remainder_degree (L)
  41. 0041specialize prime_field_polynomial_division_remainder_degree (bb)
  42. 0042specialize prime_field_polynomial_division_remainder_degree (bc)
  43. 0043specialize prime_field_polynomial_division_remainder_degree (d)
  44. 0044specialize prime_field_polynomial_division_remainder_degree (x)
  45. 0045specialize prime_field_polynomial_division_remainder_degree (x1)
  46. 0046specialize prime_field_polynomial_division_remainder_degree (x2)
  47. 0047specialize prime_field_polynomial_division_remainder_degree (x3)
  48. 0048specialize prime_field_polynomial_division_remainder_degree (x4)
  49. 0049specialize prime_field_polynomial_division_remainder_degree (x5)
  50. 0050apply prime_field_polynomial_division_remainder_degree
  51. 0051exact hp
  52. 0052exact h_witness_witness_witness_witness_witness_witness