PG0070

prime_field_polynomial_right_divides_represented_factorization

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

Trim the actual quotient, construct an independent proper-length product, and transport formal coefficients. Its genuine nonzero degree e satisfies e+d=a; no quotient degree or domain cancellation is assumed.

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 db dc D d ab ac L a. (~((p) = 1) /\ forall pfa_factor_left_factor_prime pfa_factor_right_factor_prime. (p) = pfa_factor_left_factor_prime * pfa_factor_right_factor_prime -> pfa_factor_left_factor_prime = 1 \/ pfa_factor_right_factor_prime = 1) -> ((((D)=S (d)) /\ (((forall fom_index_pfp_factor_divisorcoefficients. (exists fom_gap_pfp_factor_divisorcoefficients_index_bound. fom_gap_pfp_factor_divisorcoefficients_index_bound + S (fom_index_pfp_factor_divisorcoefficients) = D) -> exists fom_value_pfp_factor_divisorcoefficients. ((((exists fom_beta_height_pfp_factor_divisorcoefficients_entry. fom_beta_height_pfp_factor_divisorcoefficients_entry + S (fom_value_pfp_factor_divisorcoefficients) = S ((S (fom_index_pfp_factor_divisorcoefficients)) * dc)) /\ exists fom_beta_quotient_pfp_factor_divisorcoefficients_entry. db = fom_beta_quotient_pfp_factor_divisorcoefficients_entry * S ((S (fom_index_pfp_factor_divisorcoefficients)) * dc) + (fom_value_pfp_factor_divisorcoefficients))) /\ (exists fom_gap_pfp_factor_divisorcoefficients_value_bound. fom_gap_pfp_factor_divisorcoefficients_value_bound + S (fom_value_pfp_factor_divisorcoefficients) = p))) /\ ((exists pfd_leading_factor_divisor. ((((exists ff_h_pfp_factor_divisorentry. ff_h_pfp_factor_divisorentry + S (pfd_leading_factor_divisor) = S ((S (0)) * dc)) /\ exists ff_q_pfp_factor_divisorentry. db = ff_q_pfp_factor_divisorentry * S ((S (0)) * dc) + (pfd_leading_factor_divisor))) /\ ((~(pfd_leading_factor_divisor=0)))))))))) -> ((((L)=S (a)) /\ (((forall fom_index_pfp_factor_targetcoefficients. (exists fom_gap_pfp_factor_targetcoefficients_index_bound. fom_gap_pfp_factor_targetcoefficients_index_bound + S (fom_index_pfp_factor_targetcoefficients) = L) -> exists fom_value_pfp_factor_targetcoefficients. ((((exists fom_beta_height_pfp_factor_targetcoefficients_entry. fom_beta_height_pfp_factor_targetcoefficients_entry + S (fom_value_pfp_factor_targetcoefficients) = S ((S (fom_index_pfp_factor_targetcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_factor_targetcoefficients_entry. ab = fom_beta_quotient_pfp_factor_targetcoefficients_entry * S ((S (fom_index_pfp_factor_targetcoefficients)) * ac) + (fom_value_pfp_factor_targetcoefficients))) /\ (exists fom_gap_pfp_factor_targetcoefficients_value_bound. fom_gap_pfp_factor_targetcoefficients_value_bound + S (fom_value_pfp_factor_targetcoefficients) = p))) /\ ((exists pfd_leading_factor_target. ((((exists ff_h_pfp_factor_targetentry. ff_h_pfp_factor_targetentry + S (pfd_leading_factor_target) = S ((S (0)) * ac)) /\ exists ff_q_pfp_factor_targetentry. ab = ff_q_pfp_factor_targetentry * S ((S (0)) * ac) + (pfd_leading_factor_target))) /\ ((~(pfd_leading_factor_target=0)))))))))) -> (((forall fom_index_pfp_factor_divisibility_canonical. (exists fom_gap_pfp_factor_divisibility_canonical_index_bound. fom_gap_pfp_factor_divisibility_canonical_index_bound + S (fom_index_pfp_factor_divisibility_canonical) = L) -> exists fom_value_pfp_factor_divisibility_canonical. ((((exists fom_beta_height_pfp_factor_divisibility_canonical_entry. fom_beta_height_pfp_factor_divisibility_canonical_entry + S (fom_value_pfp_factor_divisibility_canonical) = S ((S (fom_index_pfp_factor_divisibility_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_factor_divisibility_canonical_entry. ab = fom_beta_quotient_pfp_factor_divisibility_canonical_entry * S ((S (fom_index_pfp_factor_divisibility_canonical)) * ac) + (fom_value_pfp_factor_divisibility_canonical))) /\ (exists fom_gap_pfp_factor_divisibility_canonical_value_bound. fom_gap_pfp_factor_divisibility_canonical_value_bound + S (fom_value_pfp_factor_divisibility_canonical) = p))) /\ ((exists pfgu_qb_factor_divisibility pfgu_qc_factor_divisibility pfgu_Q_factor_divisibility pfgu_pb_factor_divisibility pfgu_pc_factor_divisibility pfgu_P_factor_divisibility. ((((forall fom_index_pfp_factor_divisibility_productleft. (exists fom_gap_pfp_factor_divisibility_productleft_index_bound. fom_gap_pfp_factor_divisibility_productleft_index_bound + S (fom_index_pfp_factor_divisibility_productleft) = pfgu_Q_factor_divisibility) -> exists fom_value_pfp_factor_divisibility_productleft. ((((exists fom_beta_height_pfp_factor_divisibility_productleft_entry. fom_beta_height_pfp_factor_divisibility_productleft_entry + S (fom_value_pfp_factor_divisibility_productleft) = S ((S (fom_index_pfp_factor_divisibility_productleft)) * pfgu_qc_factor_divisibility)) /\ exists fom_beta_quotient_pfp_factor_divisibility_productleft_entry. pfgu_qb_factor_divisibility = fom_beta_quotient_pfp_factor_divisibility_productleft_entry * S ((S (fom_index_pfp_factor_divisibility_productleft)) * pfgu_qc_factor_divisibility) + (fom_value_pfp_factor_divisibility_productleft))) /\ (exists fom_gap_pfp_factor_divisibility_productleft_value_bound. fom_gap_pfp_factor_divisibility_productleft_value_bound + S (fom_value_pfp_factor_divisibility_productleft) = p))) /\ (((forall fom_index_pfp_factor_divisibility_productright. (exists fom_gap_pfp_factor_divisibility_productright_index_bound. fom_gap_pfp_factor_divisibility_productright_index_bound + S (fom_index_pfp_factor_divisibility_productright) = D) -> exists fom_value_pfp_factor_divisibility_productright. ((((exists fom_beta_height_pfp_factor_divisibility_productright_entry. fom_beta_height_pfp_factor_divisibility_productright_entry + S (fom_value_pfp_factor_divisibility_productright) = S ((S (fom_index_pfp_factor_divisibility_productright)) * dc)) /\ exists fom_beta_quotient_pfp_factor_divisibility_productright_entry. db = fom_beta_quotient_pfp_factor_divisibility_productright_entry * S ((S (fom_index_pfp_factor_divisibility_productright)) * dc) + (fom_value_pfp_factor_divisibility_productright))) /\ (exists fom_gap_pfp_factor_divisibility_productright_value_bound. fom_gap_pfp_factor_divisibility_productright_value_bound + S (fom_value_pfp_factor_divisibility_productright) = p))) /\ (((((((pfgu_Q_factor_divisibility)=0 \/ (D)=0) /\ (((pfgu_P_factor_divisibility)=0)))) \/ (((~((pfgu_Q_factor_divisibility)=0)) /\ (((~((D)=0)) /\ (((pfgu_Q_factor_divisibility)+(D)=S (pfgu_P_factor_divisibility)))))))) /\ ((forall pfc_index_factor_divisibility_productcoefficients. (exists pfa_gap_factor_divisibility_productcoefficientsbound. pfa_gap_factor_divisibility_productcoefficientsbound + S (pfc_index_factor_divisibility_productcoefficients) = (pfgu_P_factor_divisibility)) -> exists pfc_value_factor_divisibility_productcoefficients. ((((exists ff_h_pfp_factor_divisibility_productcoefficientsentry. ff_h_pfp_factor_divisibility_productcoefficientsentry + S (pfc_value_factor_divisibility_productcoefficients) = S ((S (pfc_index_factor_divisibility_productcoefficients)) * pfgu_pc_factor_divisibility)) /\ exists ff_q_pfp_factor_divisibility_productcoefficientsentry. pfgu_pb_factor_divisibility = ff_q_pfp_factor_divisibility_productcoefficientsentry * S ((S (pfc_index_factor_divisibility_productcoefficients)) * pfgu_pc_factor_divisibility) + (pfc_value_factor_divisibility_productcoefficients))) /\ ((exists pfc_terms_code_factor_divisibility_productcoefficientscoefficient pfc_terms_scale_factor_divisibility_productcoefficientscoefficient pfc_natural_sum_factor_divisibility_productcoefficientscoefficient. ((forall pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal. (exists pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonalbound. pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonalbound + S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal) = (S (pfc_index_factor_divisibility_productcoefficients))) -> exists pfc_value_factor_divisibility_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonalentry. ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonalentry + S (pfc_value_factor_divisibility_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_divisibility_productcoefficientscoefficient)) /\ exists ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonalentry. pfc_terms_code_factor_divisibility_productcoefficientscoefficient = ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_divisibility_productcoefficientscoefficient) + (pfc_value_factor_divisibility_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm. (((pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)+pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm=(pfc_index_factor_divisibility_productcoefficients)) /\ ((((((exists pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal) = (pfgu_Q_factor_divisibility)) /\ ((((exists ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) * pfgu_qc_factor_divisibility)) /\ exists ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_factor_divisibility = ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) * pfgu_qc_factor_divisibility) + (pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_factor_divisibility)=(pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_factor_divisibility_productcoefficientscoefficientdiagonal)=pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm*pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum. ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_start. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_start. fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_factor_divisibility_productcoefficientscoefficient) = S ((S (S (pfc_index_factor_divisibility_productcoefficients))) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_factor_divisibility_productcoefficients))) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum) + (pfc_natural_sum_factor_divisibility_productcoefficientscoefficient))) /\ forall fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps = S (pfc_index_factor_divisibility_productcoefficients)) -> exists fs_a_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps fs_r_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps fs_s_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_divisibility_productcoefficientscoefficient)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_factor_divisibility_productcoefficientscoefficient = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_divisibility_productcoefficientscoefficient) + (fs_a_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum) + (fs_r_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum) + (fs_s_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps = fs_r_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps + fs_a_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_factor_divisibility_productcoefficientscoefficientresiduebound. pfa_gap_factor_divisibility_productcoefficientscoefficientresiduebound + S (pfc_value_factor_divisibility_productcoefficients) = (p)) /\ ((exists pfa_offset_left_factor_divisibility_productcoefficientscoefficientresiduecongruence pfa_offset_right_factor_divisibility_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_factor_divisibility_productcoefficientscoefficient) + (p) * pfa_offset_left_factor_divisibility_productcoefficientscoefficientresiduecongruence = (pfc_value_factor_divisibility_productcoefficients) + (p) * pfa_offset_right_factor_divisibility_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_factor_divisibility_target pfrep_left_factor_divisibility_target pfrep_right_factor_divisibility_target. ((exists pfrep_position_factor_divisibility_targetfirst. ((pfrep_position_factor_divisibility_targetfirst+S (pfrep_power_factor_divisibility_target)=(pfgu_P_factor_divisibility)) /\ ((((exists ff_h_pfp_factor_divisibility_targetfirstentry. ff_h_pfp_factor_divisibility_targetfirstentry + S (pfrep_left_factor_divisibility_target) = S ((S (pfrep_position_factor_divisibility_targetfirst)) * pfgu_pc_factor_divisibility)) /\ exists ff_q_pfp_factor_divisibility_targetfirstentry. pfgu_pb_factor_divisibility = ff_q_pfp_factor_divisibility_targetfirstentry * S ((S (pfrep_position_factor_divisibility_targetfirst)) * pfgu_pc_factor_divisibility) + (pfrep_left_factor_divisibility_target)))))) \/ (((exists pfrep_gap_factor_divisibility_targetfirstoutside. pfrep_gap_factor_divisibility_targetfirstoutside+(pfgu_P_factor_divisibility)=(pfrep_power_factor_divisibility_target)) /\ (((pfrep_left_factor_divisibility_target)=0))))) -> ((exists pfrep_position_factor_divisibility_targetsecond. ((pfrep_position_factor_divisibility_targetsecond+S (pfrep_power_factor_divisibility_target)=(L)) /\ ((((exists ff_h_pfp_factor_divisibility_targetsecondentry. ff_h_pfp_factor_divisibility_targetsecondentry + S (pfrep_right_factor_divisibility_target) = S ((S (pfrep_position_factor_divisibility_targetsecond)) * ac)) /\ exists ff_q_pfp_factor_divisibility_targetsecondentry. ab = ff_q_pfp_factor_divisibility_targetsecondentry * S ((S (pfrep_position_factor_divisibility_targetsecond)) * ac) + (pfrep_right_factor_divisibility_target)))))) \/ (((exists pfrep_gap_factor_divisibility_targetsecondoutside. pfrep_gap_factor_divisibility_targetsecondoutside+(L)=(pfrep_power_factor_divisibility_target)) /\ (((pfrep_right_factor_divisibility_target)=0))))) -> pfrep_left_factor_divisibility_target=pfrep_right_factor_divisibility_target))))))) -> (exists pfgu_qb_factor_result pfgu_qc_factor_result pfgu_e_factor_result pfgu_pb_factor_result pfgu_pc_factor_result. (((((S (pfgu_e_factor_result))=S (pfgu_e_factor_result)) /\ (((forall fom_index_pfp_factor_result_quotientcoefficients. (exists fom_gap_pfp_factor_result_quotientcoefficients_index_bound. fom_gap_pfp_factor_result_quotientcoefficients_index_bound + S (fom_index_pfp_factor_result_quotientcoefficients) = S (pfgu_e_factor_result)) -> exists fom_value_pfp_factor_result_quotientcoefficients. ((((exists fom_beta_height_pfp_factor_result_quotientcoefficients_entry. fom_beta_height_pfp_factor_result_quotientcoefficients_entry + S (fom_value_pfp_factor_result_quotientcoefficients) = S ((S (fom_index_pfp_factor_result_quotientcoefficients)) * pfgu_qc_factor_result)) /\ exists fom_beta_quotient_pfp_factor_result_quotientcoefficients_entry. pfgu_qb_factor_result = fom_beta_quotient_pfp_factor_result_quotientcoefficients_entry * S ((S (fom_index_pfp_factor_result_quotientcoefficients)) * pfgu_qc_factor_result) + (fom_value_pfp_factor_result_quotientcoefficients))) /\ (exists fom_gap_pfp_factor_result_quotientcoefficients_value_bound. fom_gap_pfp_factor_result_quotientcoefficients_value_bound + S (fom_value_pfp_factor_result_quotientcoefficients) = p))) /\ ((exists pfd_leading_factor_result_quotient. ((((exists ff_h_pfp_factor_result_quotiententry. ff_h_pfp_factor_result_quotiententry + S (pfd_leading_factor_result_quotient) = S ((S (0)) * pfgu_qc_factor_result)) /\ exists ff_q_pfp_factor_result_quotiententry. pfgu_qb_factor_result = ff_q_pfp_factor_result_quotiententry * S ((S (0)) * pfgu_qc_factor_result) + (pfd_leading_factor_result_quotient))) /\ ((~(pfd_leading_factor_result_quotient=0)))))))))) /\ (((((forall fom_index_pfp_factor_result_productleft. (exists fom_gap_pfp_factor_result_productleft_index_bound. fom_gap_pfp_factor_result_productleft_index_bound + S (fom_index_pfp_factor_result_productleft) = S (pfgu_e_factor_result)) -> exists fom_value_pfp_factor_result_productleft. ((((exists fom_beta_height_pfp_factor_result_productleft_entry. fom_beta_height_pfp_factor_result_productleft_entry + S (fom_value_pfp_factor_result_productleft) = S ((S (fom_index_pfp_factor_result_productleft)) * pfgu_qc_factor_result)) /\ exists fom_beta_quotient_pfp_factor_result_productleft_entry. pfgu_qb_factor_result = fom_beta_quotient_pfp_factor_result_productleft_entry * S ((S (fom_index_pfp_factor_result_productleft)) * pfgu_qc_factor_result) + (fom_value_pfp_factor_result_productleft))) /\ (exists fom_gap_pfp_factor_result_productleft_value_bound. fom_gap_pfp_factor_result_productleft_value_bound + S (fom_value_pfp_factor_result_productleft) = p))) /\ (((forall fom_index_pfp_factor_result_productright. (exists fom_gap_pfp_factor_result_productright_index_bound. fom_gap_pfp_factor_result_productright_index_bound + S (fom_index_pfp_factor_result_productright) = D) -> exists fom_value_pfp_factor_result_productright. ((((exists fom_beta_height_pfp_factor_result_productright_entry. fom_beta_height_pfp_factor_result_productright_entry + S (fom_value_pfp_factor_result_productright) = S ((S (fom_index_pfp_factor_result_productright)) * dc)) /\ exists fom_beta_quotient_pfp_factor_result_productright_entry. db = fom_beta_quotient_pfp_factor_result_productright_entry * S ((S (fom_index_pfp_factor_result_productright)) * dc) + (fom_value_pfp_factor_result_productright))) /\ (exists fom_gap_pfp_factor_result_productright_value_bound. fom_gap_pfp_factor_result_productright_value_bound + S (fom_value_pfp_factor_result_productright) = p))) /\ (((((((S (pfgu_e_factor_result))=0 \/ (D)=0) /\ (((S (a))=0)))) \/ (((~((S (pfgu_e_factor_result))=0)) /\ (((~((D)=0)) /\ (((S (pfgu_e_factor_result))+(D)=S (S (a))))))))) /\ ((forall pfc_index_factor_result_productcoefficients. (exists pfa_gap_factor_result_productcoefficientsbound. pfa_gap_factor_result_productcoefficientsbound + S (pfc_index_factor_result_productcoefficients) = (S (a))) -> exists pfc_value_factor_result_productcoefficients. ((((exists ff_h_pfp_factor_result_productcoefficientsentry. ff_h_pfp_factor_result_productcoefficientsentry + S (pfc_value_factor_result_productcoefficients) = S ((S (pfc_index_factor_result_productcoefficients)) * pfgu_pc_factor_result)) /\ exists ff_q_pfp_factor_result_productcoefficientsentry. pfgu_pb_factor_result = ff_q_pfp_factor_result_productcoefficientsentry * S ((S (pfc_index_factor_result_productcoefficients)) * pfgu_pc_factor_result) + (pfc_value_factor_result_productcoefficients))) /\ ((exists pfc_terms_code_factor_result_productcoefficientscoefficient pfc_terms_scale_factor_result_productcoefficientscoefficient pfc_natural_sum_factor_result_productcoefficientscoefficient. ((forall pfc_index_factor_result_productcoefficientscoefficientdiagonal. (exists pfa_gap_factor_result_productcoefficientscoefficientdiagonalbound. pfa_gap_factor_result_productcoefficientscoefficientdiagonalbound + S (pfc_index_factor_result_productcoefficientscoefficientdiagonal) = (S (pfc_index_factor_result_productcoefficients))) -> exists pfc_value_factor_result_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_factor_result_productcoefficientscoefficientdiagonalentry. ff_h_pfp_factor_result_productcoefficientscoefficientdiagonalentry + S (pfc_value_factor_result_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_factor_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_result_productcoefficientscoefficient)) /\ exists ff_q_pfp_factor_result_productcoefficientscoefficientdiagonalentry. pfc_terms_code_factor_result_productcoefficientscoefficient = ff_q_pfp_factor_result_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_factor_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_result_productcoefficientscoefficient) + (pfc_value_factor_result_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm pfc_left_factor_result_productcoefficientscoefficientdiagonalterm pfc_right_factor_result_productcoefficientscoefficientdiagonalterm. (((pfc_index_factor_result_productcoefficientscoefficientdiagonal)+pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm=(pfc_index_factor_result_productcoefficients)) /\ ((((((exists pfa_gap_factor_result_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_factor_result_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_factor_result_productcoefficientscoefficientdiagonal) = (S (pfgu_e_factor_result))) /\ ((((exists ff_h_pfp_factor_result_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_factor_result_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_factor_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_factor_result_productcoefficientscoefficientdiagonal)) * pfgu_qc_factor_result)) /\ exists ff_q_pfp_factor_result_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_factor_result = ff_q_pfp_factor_result_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_factor_result_productcoefficientscoefficientdiagonal)) * pfgu_qc_factor_result) + (pfc_left_factor_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_result_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_factor_result_productcoefficientscoefficientdiagonaltermleftoutside+(S (pfgu_e_factor_result))=(pfc_index_factor_result_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_factor_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_factor_result_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_factor_result_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_factor_result_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_factor_result_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_factor_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_factor_result_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_factor_result_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_factor_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_result_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_factor_result_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_factor_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_factor_result_productcoefficientscoefficientdiagonal)=pfc_left_factor_result_productcoefficientscoefficientdiagonalterm*pfc_right_factor_result_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_factor_result_productcoefficientscoefficientsum fs_v_pfc_factor_result_productcoefficientscoefficientsum. ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_start. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_start. fs_u_pfc_factor_result_productcoefficientscoefficientsum = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_factor_result_productcoefficientscoefficient) = S ((S (S (pfc_index_factor_result_productcoefficients))) * fs_v_pfc_factor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_factor_result_productcoefficientscoefficientsum = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_factor_result_productcoefficients))) * fs_v_pfc_factor_result_productcoefficientscoefficientsum) + (pfc_natural_sum_factor_result_productcoefficientscoefficient))) /\ forall fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_factor_result_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_factor_result_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps = S (pfc_index_factor_result_productcoefficients)) -> exists fs_a_pfc_factor_result_productcoefficientscoefficientsum_body_steps fs_r_pfc_factor_result_productcoefficientscoefficientsum_body_steps fs_s_pfc_factor_result_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_factor_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_result_productcoefficientscoefficient)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_factor_result_productcoefficientscoefficient = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_result_productcoefficientscoefficient) + (fs_a_pfc_factor_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_factor_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_factor_result_productcoefficientscoefficientsum = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum) + (fs_r_pfc_factor_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_factor_result_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_factor_result_productcoefficientscoefficientsum = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum) + (fs_s_pfc_factor_result_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_factor_result_productcoefficientscoefficientsum_body_steps = fs_r_pfc_factor_result_productcoefficientscoefficientsum_body_steps + fs_a_pfc_factor_result_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_factor_result_productcoefficientscoefficientresiduebound. pfa_gap_factor_result_productcoefficientscoefficientresiduebound + S (pfc_value_factor_result_productcoefficients) = (p)) /\ ((exists pfa_offset_left_factor_result_productcoefficientscoefficientresiduecongruence pfa_offset_right_factor_result_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_factor_result_productcoefficientscoefficient) + (p) * pfa_offset_left_factor_result_productcoefficientscoefficientresiduecongruence = (pfc_value_factor_result_productcoefficients) + (p) * pfa_offset_right_factor_result_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((forall pfrep_power_factor_result_equivalent pfrep_left_factor_result_equivalent pfrep_right_factor_result_equivalent. ((exists pfrep_position_factor_result_equivalentfirst. ((pfrep_position_factor_result_equivalentfirst+S (pfrep_power_factor_result_equivalent)=(S (a))) /\ ((((exists ff_h_pfp_factor_result_equivalentfirstentry. ff_h_pfp_factor_result_equivalentfirstentry + S (pfrep_left_factor_result_equivalent) = S ((S (pfrep_position_factor_result_equivalentfirst)) * pfgu_pc_factor_result)) /\ exists ff_q_pfp_factor_result_equivalentfirstentry. pfgu_pb_factor_result = ff_q_pfp_factor_result_equivalentfirstentry * S ((S (pfrep_position_factor_result_equivalentfirst)) * pfgu_pc_factor_result) + (pfrep_left_factor_result_equivalent)))))) \/ (((exists pfrep_gap_factor_result_equivalentfirstoutside. pfrep_gap_factor_result_equivalentfirstoutside+(S (a))=(pfrep_power_factor_result_equivalent)) /\ (((pfrep_left_factor_result_equivalent)=0))))) -> ((exists pfrep_position_factor_result_equivalentsecond. ((pfrep_position_factor_result_equivalentsecond+S (pfrep_power_factor_result_equivalent)=(L)) /\ ((((exists ff_h_pfp_factor_result_equivalentsecondentry. ff_h_pfp_factor_result_equivalentsecondentry + S (pfrep_right_factor_result_equivalent) = S ((S (pfrep_position_factor_result_equivalentsecond)) * ac)) /\ exists ff_q_pfp_factor_result_equivalentsecondentry. ab = ff_q_pfp_factor_result_equivalentsecondentry * S ((S (pfrep_position_factor_result_equivalentsecond)) * ac) + (pfrep_right_factor_result_equivalent)))))) \/ (((exists pfrep_gap_factor_result_equivalentsecondoutside. pfrep_gap_factor_result_equivalentsecondoutside+(L)=(pfrep_power_factor_result_equivalent)) /\ (((pfrep_right_factor_result_equivalent)=0))))) -> pfrep_left_factor_result_equivalent=pfrep_right_factor_result_equivalent) /\ (((pfgu_e_factor_result)+(d)=(a)))))))))

Constructive proof overview

Generated structural guide

Trim the actual quotient, construct an independent proper-length product, and transport formal coefficients. Its genuine nonzero degree e satisfies e+d=a; no quotient degree or domain cancellation is assumed.

The unchanged tactic script uses 13 declared prerequisites and contains 235 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_nonzero Alpha theorem; checked-use authorized prime_field_polynomial_trim_exists Alpha theorem; checked-use authorized prime_field_polynomial_trim_output_coefficients Alpha theorem; checked-use authorized prime_field_polynomial_trim_equivalent Alpha theorem; checked-use authorized polynomial_product_length_exists Alpha theorem; checked-use authorized prime_field_polynomial_convolution_at_length_exists Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_transitive Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_symmetric Alpha theorem; checked-use authorized prime_field_polynomial_convolution_equivalent_congruent_left Alpha theorem; checked-use authorized PG006F prime_field_polynomial_product_equivalent_nonzero_left_nonempty prime_field_polynomial_trim_nonempty_degree_exists Alpha theorem; checked-use authorized prime_field_polynomial_convolution_represented_degree Alpha theorem; checked-use authorized PG006E prime_field_polynomial_equivalent_represented_degrees_equal

Direct dependents

PG0071 prime_field_polynomial_right_divides_represented_degree_bound PG0073 prime_field_polynomial_monic_equal_degree_right_divides_equivalent

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

235 script commands · 50 reading checkpoints · 18 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 product equivalent nonzero left nonemptyprime field polynomial equivalent represented degrees equal

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 db
  3. L3
    intro dc
  4. L4
    intro D
  5. L5
    intro d
  6. L6
    intro ab
  7. L7
    intro ac
  8. L8
    intro L
  9. L9
    intro a
  10. L10
    intro hp
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hd
  2. L12
    intro ha
  3. L13
    intro hrd
03Establish hpnL14–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime nonzero.

  1. L14
    have hpn : ~(p=0)
  2. L15
    intro hpzero
  3. L16
    specialize prime_nonzero (p)
  4. L17
    apply prime_nonzero
  5. L18
    exact hp
  6. L19
    exact hpzero
04Establish hdboundL20–20

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

  1. L20
    have hdbound : BetaPrefixInto(db,dc,D,p)Definitions: BetaPrefixInto
05Separate the logical casesL21–22

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

  1. L21
    cases hd
  2. L22
    cases hd_right
06Use earlier factsL23–23

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

  1. L23
    exact hd_right_left
07Separate the logical casesL24–31

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

  1. L24
    cases hrd
  2. L25
    cases hrd_right
  3. L26
    cases hrd_right_witness
  4. L27
    cases hrd_right_witness_witness
  5. L28
    cases hrd_right_witness_witness_witness
  6. L29
    cases hrd_right_witness_witness_witness_witness
  7. L30
    cases hrd_right_witness_witness_witness_witness_witness
  8. L31
    cases hrd_right_witness_witness_witness_witness_witness_witness
08Establish hqboundL32–32

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

  1. L32
    have hqbound : BetaPrefixInto(x,x1,x2,p)Definitions: BetaPrefixInto
09Separate the logical casesL33–35

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

  1. L33
    cases hrd_right_witness_witness_witness_witness_witness_witness_left
  2. L34
    cases hrd_right_witness_witness_witness_witness_witness_witness_left_right
  3. L35
    cases hrd_right_witness_witness_witness_witness_witness_witness_left_right_right
10Use earlier factsL36–36

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

  1. L36
    exact hrd_right_witness_witness_witness_witness_witness_witness_left_left
11Establish htL37–43

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

  1. L37
    have ht : ∃ t. ∃ tb. ∃ tc. ∃ T. FpPolynomialTrim(p,x,x1,x2,t,tb,tc,T)Definitions: FpPolynomialTrim
  2. L38
    specialize prime_field_polynomial_trim_exists (p)
  3. L39
    specialize prime_field_polynomial_trim_exists (x)
  4. L40
    specialize prime_field_polynomial_trim_exists (x1)
  5. L41
    specialize prime_field_polynomial_trim_exists (x2)
  6. L42
    apply prime_field_polynomial_trim_exists
  7. L43
    exact hqbound
12Separate the logical casesL44–47

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

  1. L44
    cases ht
  2. L45
    cases ht_witness
  3. L46
    cases ht_witness_witness
  4. L47
    cases ht_witness_witness_witness
13Establish htboundL48–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial trim output coefficients.

  1. L48
    have htbound : BetaPrefixInto(x7,x8,x9,p)Definitions: BetaPrefixInto
  2. L49
    specialize prime_field_polynomial_trim_output_coefficients (p)
  3. L50
    specialize prime_field_polynomial_trim_output_coefficients (x)
  4. L51
    specialize prime_field_polynomial_trim_output_coefficients (x1)
  5. L52
    specialize prime_field_polynomial_trim_output_coefficients (x2)
  6. L53
    specialize prime_field_polynomial_trim_output_coefficients (x6)
  7. L54
    specialize prime_field_polynomial_trim_output_coefficients (x7)
  8. L55
    specialize prime_field_polynomial_trim_output_coefficients (x8)
  9. L56
    specialize prime_field_polynomial_trim_output_coefficients (x9)
  10. L57
    apply prime_field_polynomial_trim_output_coefficients
14Use earlier factsL58–58

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

  1. L58
    exact ht_witness_witness_witness_witness
15Establish hqeL59–68

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

  1. L59
    have hqe : PolynomialEquivalent(x,x1,x2,x7,x8,x9)Definitions: PolynomialEquivalent
  2. L60
    specialize prime_field_polynomial_trim_equivalent (p)
  3. L61
    specialize prime_field_polynomial_trim_equivalent (x)
  4. L62
    specialize prime_field_polynomial_trim_equivalent (x1)
  5. L63
    specialize prime_field_polynomial_trim_equivalent (x2)
  6. L64
    specialize prime_field_polynomial_trim_equivalent (x6)
  7. L65
    specialize prime_field_polynomial_trim_equivalent (x7)
  8. L66
    specialize prime_field_polynomial_trim_equivalent (x8)
  9. L67
    specialize prime_field_polynomial_trim_equivalent (x9)
  10. L68
    apply prime_field_polynomial_trim_equivalent
16Use earlier factsL69–69

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

  1. L69
    exact ht_witness_witness_witness_witness
17Establish hplenL70–73

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.

  1. L70
    have hplen : exists N. ((((x9)=0 \/ (D)=0) /\ (((N)=0)))) \/ (((~((x9)=0)) /\ (((~((D)=0)) /\ (((x9)+(D)=S (N)))))))
  2. L71
    specialize polynomial_product_length_exists (x9)
  3. L72
    specialize polynomial_product_length_exists (D)
  4. L73
    apply polynomial_product_length_exists
18Separate the logical casesL74–74

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

  1. L74
    cases hplen
19Establish hpnewL75–84

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

  1. L75
    have hpnew : ∃ vb. ∃ vc. FpPolyProduct(p,x7,x8,x9,db,dc,D,vb,vc,x10)Definitions: FpPolyProduct
  2. L76
    specialize prime_field_polynomial_convolution_at_length_exists (p)
  3. L77
    specialize prime_field_polynomial_convolution_at_length_exists (x7)
  4. L78
    specialize prime_field_polynomial_convolution_at_length_exists (x8)
  5. L79
    specialize prime_field_polynomial_convolution_at_length_exists (x9)
  6. L80
    specialize prime_field_polynomial_convolution_at_length_exists (db)
  7. L81
    specialize prime_field_polynomial_convolution_at_length_exists (dc)
  8. L82
    specialize prime_field_polynomial_convolution_at_length_exists (D)
  9. L83
    specialize prime_field_polynomial_convolution_at_length_exists (x10)
  10. L84
    apply prime_field_polynomial_convolution_at_length_exists
20Use earlier factsL85–88

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

  1. L85
    exact hpn
  2. L86
    exact htbound
  3. L87
    exact hdbound
  4. L88
    exact hplen_witness
21Separate the logical casesL89–90

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

  1. L89
    cases hpnew
  2. L90
    cases hpnew_witness
22Establish hequivL91–100

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

  1. L91
    have hequiv : PolynomialEquivalent(x11,x12,x10,ab,ac,L)Definitions: PolynomialEquivalent
  2. L92
    specialize prime_field_polynomial_equivalent_transitive (x11)
  3. L93
    specialize prime_field_polynomial_equivalent_transitive (x12)
  4. L94
    specialize prime_field_polynomial_equivalent_transitive (x10)
  5. L95
    specialize prime_field_polynomial_equivalent_transitive (x3)
  6. L96
    specialize prime_field_polynomial_equivalent_transitive (x4)
  7. L97
    specialize prime_field_polynomial_equivalent_transitive (x5)
  8. L98
    specialize prime_field_polynomial_equivalent_transitive (ab)
  9. L99
    specialize prime_field_polynomial_equivalent_transitive (ac)
  10. L100
    specialize prime_field_polynomial_equivalent_transitive (L)
23Use earlier factsL101–110

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

  1. L101
    apply prime_field_polynomial_equivalent_transitive
  2. L102
    specialize prime_field_polynomial_equivalent_symmetric (x3)
  3. L103
    specialize prime_field_polynomial_equivalent_symmetric (x4)
  4. L104
    specialize prime_field_polynomial_equivalent_symmetric (x5)
  5. L105
    specialize prime_field_polynomial_equivalent_symmetric (x11)
  6. L106
    specialize prime_field_polynomial_equivalent_symmetric (x12)
  7. L107
    specialize prime_field_polynomial_equivalent_symmetric (x10)
  8. L108
    apply prime_field_polynomial_equivalent_symmetric
  9. L109
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (p)
  10. L110
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x)
24Use earlier factsL111–120

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

  1. L111
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x1)
  2. L112
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x2)
  3. L113
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (db)
  4. L114
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (dc)
  5. L115
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (D)
  6. L116
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x3)
  7. L117
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x4)
  8. L118
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x5)
  9. L119
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x7)
  10. L120
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x8)
25Use earlier factsL121–130

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

  1. L121
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x9)
  2. L122
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x11)
  3. L123
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x12)
  4. L124
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x10)
  5. L125
    apply prime_field_polynomial_convolution_equivalent_congruent_left
  6. L126
    exact hpn
  7. L127
    exact hqe
  8. L128
    exact hrd_right_witness_witness_witness_witness_witness_witness_left
  9. L129
    exact hpnew_witness_witness
  10. L130
    exact hrd_right_witness_witness_witness_witness_witness_witness_right
26Establish hnL131–140

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

  1. L131
    have hn : ~(x9=0)
  2. L132
    intro htzero
  3. L133
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (p)
  4. L134
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x7)
  5. L135
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x8)
  6. L136
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x9)
  7. L137
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (db)
  8. L138
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (dc)
  9. L139
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (D)
  10. L140
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x11)
27Use earlier factsL141–150

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

  1. L141
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x12)
  2. L142
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x10)
  3. L143
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (ab)
  4. L144
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (ac)
  5. L145
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (L)
  6. L146
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (a)
  7. L147
    apply prime_field_polynomial_product_equivalent_nonzero_left_nonempty
  8. L148
    exact ha
  9. L149
    exact hpnew_witness_witness
  10. L150
    exact hequiv
28Use earlier factsL151–151

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

  1. L151
    exact htzero
29Establish hqdL152–161

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

  1. L152
    have hqd : ∃ e. FpRepresentedDegree(p,x7,x8,x9,e)Definitions: FpRepresentedDegree
  2. L153
    specialize prime_field_polynomial_trim_nonempty_degree_exists (p)
  3. L154
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x)
  4. L155
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x1)
  5. L156
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x2)
  6. L157
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x6)
  7. L158
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x7)
  8. L159
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x8)
  9. L160
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x9)
  10. L161
    apply prime_field_polynomial_trim_nonempty_degree_exists
30Use earlier factsL162–163

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

  1. L162
    exact ht_witness_witness_witness_witness
  2. L163
    exact hn
31Separate the logical casesL164–164

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

  1. L164
    cases hqd
32Establish hpdL165–174

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

  1. L165
    have hpd : FpRepresentedDegree(p,x11,x12,x10,x13 + d)Definitions: FpRepresentedDegree
  2. L166
    specialize prime_field_polynomial_convolution_represented_degree (p)
  3. L167
    specialize prime_field_polynomial_convolution_represented_degree (x7)
  4. L168
    specialize prime_field_polynomial_convolution_represented_degree (x8)
  5. L169
    specialize prime_field_polynomial_convolution_represented_degree (x9)
  6. L170
    specialize prime_field_polynomial_convolution_represented_degree (x13)
  7. L171
    specialize prime_field_polynomial_convolution_represented_degree (db)
  8. L172
    specialize prime_field_polynomial_convolution_represented_degree (dc)
  9. L173
    specialize prime_field_polynomial_convolution_represented_degree (D)
  10. L174
    specialize prime_field_polynomial_convolution_represented_degree (d)
33Use earlier factsL175–182

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

  1. L175
    specialize prime_field_polynomial_convolution_represented_degree (x11)
  2. L176
    specialize prime_field_polynomial_convolution_represented_degree (x12)
  3. L177
    specialize prime_field_polynomial_convolution_represented_degree (x10)
  4. L178
    apply prime_field_polynomial_convolution_represented_degree
  5. L179
    exact hp
  6. L180
    exact hqd_witness
  7. L181
    exact hd
  8. L182
    exact hpnew_witness_witness
34Establish hsumL183–192

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

  1. L183
    have hsum : x13+d=a
  2. L184
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (p)
  3. L185
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (x11)
  4. L186
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (x12)
  5. L187
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (x10)
  6. L188
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (x13+d)
  7. L189
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (ab)
  8. L190
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (ac)
  9. L191
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (L)
  10. L192
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (a)
35Use earlier factsL193–196

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

  1. L193
    apply prime_field_polynomial_equivalent_represented_degrees_equal
  2. L194
    exact hpd
  3. L195
    exact ha
  4. L196
    exact hequiv
36Establish hqlenL197–197

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

  1. L197
    have hqlen : x9=S x13
37Separate the logical casesL198–198

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

  1. L198
    cases hqd_witness
38Use earlier factsL199–199

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

  1. L199
    exact hqd_witness_left
39Establish hplen2L200–200

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

  1. L200
    have hplen2 : x10=S a
40Separate the logical casesL201–201

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

  1. L201
    cases hpd
41Calculate and transport equalitiesL202–204

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L202
    rewrite hpd_left
  2. L203
    rewrite hsum
  3. L204
    refl
42Construct an explicit witnessL205–209

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

  1. L205
    exists x7
  2. L206
    exists x8
  3. L207
    exists x13
  4. L208
    exists x11
  5. L209
    exists x12
43Separate the logical casesL210–210

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

  1. L210
    split
44Establish hqdnewL211–215

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

  1. L211
    have hqdnew : FpRepresentedDegree(p,x7,x8,x9,x13)Definitions: FpRepresentedDegree
  2. L212
    exact hqd_witness
  3. L213
    rewrite hqlen at hqdnew
  4. L214
    rewrite hqlen at hqdnew
  5. L215
    exact hqdnew
45Separate the logical casesL216–216

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

  1. L216
    split
46Establish hcpL217–226

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

  1. L217
    have hcp : FpPolyProduct(p,x7,x8,x9,db,dc,D,x11,x12,x10)Definitions: FpPolyProduct
  2. L218
    exact hpnew_witness_witness
  3. L219
    rewrite hqlen at hcp
  4. L220
    rewrite hqlen at hcp
  5. L221
    rewrite hqlen at hcp
  6. L222
    rewrite hqlen at hcp
  7. L223
    rewrite hqlen at hcp
  8. L224
    rewrite hqlen at hcp
  9. L225
    rewrite hplen2 at hcp
  10. L226
    rewrite hplen2 at hcp
47Calculate and transport equalitiesL227–227

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L227
    rewrite hplen2 at hcp
48Use earlier factsL228–228

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

  1. L228
    exact hcp
49Separate the logical casesL229–229

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

  1. L229
    split
50Establish hepL230–235

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

  1. L230
    have hep : PolynomialEquivalent(x11,x12,x10,ab,ac,L)Definitions: PolynomialEquivalent
  2. L231
    exact hequiv
  3. L232
    rewrite hplen2 at hep
  4. L233
    rewrite hplen2 at hep
  5. L234
    exact hep
  6. L235
    exact hsum

Library-wide reading audit

Original exact command ledger · 235 lines
  1. 0001intro p
  2. 0002intro db
  3. 0003intro dc
  4. 0004intro D
  5. 0005intro d
  6. 0006intro ab
  7. 0007intro ac
  8. 0008intro L
  9. 0009intro a
  10. 0010intro hp
  11. 0011intro hd
  12. 0012intro ha
  13. 0013intro hrd
  14. 0014have hpn : ~(p=0)
  15. 0015intro hpzero
  16. 0016specialize prime_nonzero (p)
  17. 0017apply prime_nonzero
  18. 0018exact hp
  19. 0019exact hpzero
  20. 0020have hdbound : forall fom_index_pfp_factor_divisor_bound. (exists fom_gap_pfp_factor_divisor_bound_index_bound. fom_gap_pfp_factor_divisor_bound_index_bound + S (fom_index_pfp_factor_divisor_bound) = D) -> exists fom_value_pfp_factor_divisor_bound. ((((exists fom_beta_height_pfp_factor_divisor_bound_entry. fom_beta_height_pfp_factor_divisor_bound_entry + S (fom_value_pfp_factor_divisor_bound) = S ((S (fom_index_pfp_factor_divisor_bound)) * dc)) /\ exists fom_beta_quotient_pfp_factor_divisor_bound_entry. db = fom_beta_quotient_pfp_factor_divisor_bound_entry * S ((S (fom_index_pfp_factor_divisor_bound)) * dc) + (fom_value_pfp_factor_divisor_bound))) /\ (exists fom_gap_pfp_factor_divisor_bound_value_bound. fom_gap_pfp_factor_divisor_bound_value_bound + S (fom_value_pfp_factor_divisor_bound) = p))
  21. 0021cases hd
  22. 0022cases hd_right
  23. 0023exact hd_right_left
  24. 0024cases hrd
  25. 0025cases hrd_right
  26. 0026cases hrd_right_witness
  27. 0027cases hrd_right_witness_witness
  28. 0028cases hrd_right_witness_witness_witness
  29. 0029cases hrd_right_witness_witness_witness_witness
  30. 0030cases hrd_right_witness_witness_witness_witness_witness
  31. 0031cases hrd_right_witness_witness_witness_witness_witness_witness
  32. 0032have hqbound : forall fom_index_pfp_factor_quotient_bound. (exists fom_gap_pfp_factor_quotient_bound_index_bound. fom_gap_pfp_factor_quotient_bound_index_bound + S (fom_index_pfp_factor_quotient_bound) = x2) -> exists fom_value_pfp_factor_quotient_bound. ((((exists fom_beta_height_pfp_factor_quotient_bound_entry. fom_beta_height_pfp_factor_quotient_bound_entry + S (fom_value_pfp_factor_quotient_bound) = S ((S (fom_index_pfp_factor_quotient_bound)) * x1)) /\ exists fom_beta_quotient_pfp_factor_quotient_bound_entry. x = fom_beta_quotient_pfp_factor_quotient_bound_entry * S ((S (fom_index_pfp_factor_quotient_bound)) * x1) + (fom_value_pfp_factor_quotient_bound))) /\ (exists fom_gap_pfp_factor_quotient_bound_value_bound. fom_gap_pfp_factor_quotient_bound_value_bound + S (fom_value_pfp_factor_quotient_bound) = p))
  33. 0033cases hrd_right_witness_witness_witness_witness_witness_witness_left
  34. 0034cases hrd_right_witness_witness_witness_witness_witness_witness_left_right
  35. 0035cases hrd_right_witness_witness_witness_witness_witness_witness_left_right_right
  36. 0036exact hrd_right_witness_witness_witness_witness_witness_witness_left_left
  37. 0037have ht : exists t tb tc T. (((x2)=(t)+(T)) /\ (((forall fom_index_pfp_factor_triminput. (exists fom_gap_pfp_factor_triminput_index_bound. fom_gap_pfp_factor_triminput_index_bound + S (fom_index_pfp_factor_triminput) = x2) -> exists fom_value_pfp_factor_triminput. ((((exists fom_beta_height_pfp_factor_triminput_entry. fom_beta_height_pfp_factor_triminput_entry + S (fom_value_pfp_factor_triminput) = S ((S (fom_index_pfp_factor_triminput)) * x1)) /\ exists fom_beta_quotient_pfp_factor_triminput_entry. x = fom_beta_quotient_pfp_factor_triminput_entry * S ((S (fom_index_pfp_factor_triminput)) * x1) + (fom_value_pfp_factor_triminput))) /\ (exists fom_gap_pfp_factor_triminput_value_bound. fom_gap_pfp_factor_triminput_value_bound + S (fom_value_pfp_factor_triminput) = p))) /\ (((forall pfp_repeat_index_factor_trimremoved. (exists pfa_gap_factor_trimremovedindex. pfa_gap_factor_trimremovedindex + S (pfp_repeat_index_factor_trimremoved) = (t)) -> (((exists ff_h_pfp_factor_trimremovedentry. ff_h_pfp_factor_trimremovedentry + S (0) = S ((S (pfp_repeat_index_factor_trimremoved)) * x1)) /\ exists ff_q_pfp_factor_trimremovedentry. x = ff_q_pfp_factor_trimremovedentry * S ((S (pfp_repeat_index_factor_trimremoved)) * x1) + (0)))) /\ (((forall pftrim_index_factor_trimsuffix pftrim_value_factor_trimsuffix. (exists pfa_gap_factor_trimsuffixbound. pfa_gap_factor_trimsuffixbound + S (pftrim_index_factor_trimsuffix) = (T)) -> (((exists ff_h_pfp_factor_trimsuffixsource. ff_h_pfp_factor_trimsuffixsource + S (pftrim_value_factor_trimsuffix) = S ((S ((t)+pftrim_index_factor_trimsuffix)) * x1)) /\ exists ff_q_pfp_factor_trimsuffixsource. x = ff_q_pfp_factor_trimsuffixsource * S ((S ((t)+pftrim_index_factor_trimsuffix)) * x1) + (pftrim_value_factor_trimsuffix))) -> (((exists ff_h_pfp_factor_trimsuffixoutput. ff_h_pfp_factor_trimsuffixoutput + S (pftrim_value_factor_trimsuffix) = S ((S (pftrim_index_factor_trimsuffix)) * tc)) /\ exists ff_q_pfp_factor_trimsuffixoutput. tb = ff_q_pfp_factor_trimsuffixoutput * S ((S (pftrim_index_factor_trimsuffix)) * tc) + (pftrim_value_factor_trimsuffix)))) /\ (((T)=0 \/ (exists pftrim_leading_factor_trimnormal. ((((exists ff_h_pfp_factor_trimnormalentry. ff_h_pfp_factor_trimnormalentry + S (pftrim_leading_factor_trimnormal) = S ((S (0)) * tc)) /\ exists ff_q_pfp_factor_trimnormalentry. tb = ff_q_pfp_factor_trimnormalentry * S ((S (0)) * tc) + (pftrim_leading_factor_trimnormal))) /\ ((~(pftrim_leading_factor_trimnormal=0))))))))))))))
  38. 0038specialize prime_field_polynomial_trim_exists (p)
  39. 0039specialize prime_field_polynomial_trim_exists (x)
  40. 0040specialize prime_field_polynomial_trim_exists (x1)
  41. 0041specialize prime_field_polynomial_trim_exists (x2)
  42. 0042apply prime_field_polynomial_trim_exists
  43. 0043exact hqbound
  44. 0044cases ht
  45. 0045cases ht_witness
  46. 0046cases ht_witness_witness
  47. 0047cases ht_witness_witness_witness
  48. 0048have htbound : forall fom_index_pfp_factor_trim_bound. (exists fom_gap_pfp_factor_trim_bound_index_bound. fom_gap_pfp_factor_trim_bound_index_bound + S (fom_index_pfp_factor_trim_bound) = x9) -> exists fom_value_pfp_factor_trim_bound. ((((exists fom_beta_height_pfp_factor_trim_bound_entry. fom_beta_height_pfp_factor_trim_bound_entry + S (fom_value_pfp_factor_trim_bound) = S ((S (fom_index_pfp_factor_trim_bound)) * x8)) /\ exists fom_beta_quotient_pfp_factor_trim_bound_entry. x7 = fom_beta_quotient_pfp_factor_trim_bound_entry * S ((S (fom_index_pfp_factor_trim_bound)) * x8) + (fom_value_pfp_factor_trim_bound))) /\ (exists fom_gap_pfp_factor_trim_bound_value_bound. fom_gap_pfp_factor_trim_bound_value_bound + S (fom_value_pfp_factor_trim_bound) = p))
  49. 0049specialize prime_field_polynomial_trim_output_coefficients (p)
  50. 0050specialize prime_field_polynomial_trim_output_coefficients (x)
  51. 0051specialize prime_field_polynomial_trim_output_coefficients (x1)
  52. 0052specialize prime_field_polynomial_trim_output_coefficients (x2)
  53. 0053specialize prime_field_polynomial_trim_output_coefficients (x6)
  54. 0054specialize prime_field_polynomial_trim_output_coefficients (x7)
  55. 0055specialize prime_field_polynomial_trim_output_coefficients (x8)
  56. 0056specialize prime_field_polynomial_trim_output_coefficients (x9)
  57. 0057apply prime_field_polynomial_trim_output_coefficients
  58. 0058exact ht_witness_witness_witness_witness
  59. 0059have hqe : forall pfrep_power_factor_trim_equivalent pfrep_left_factor_trim_equivalent pfrep_right_factor_trim_equivalent. ((exists pfrep_position_factor_trim_equivalentfirst. ((pfrep_position_factor_trim_equivalentfirst+S (pfrep_power_factor_trim_equivalent)=(x2)) /\ ((((exists ff_h_pfp_factor_trim_equivalentfirstentry. ff_h_pfp_factor_trim_equivalentfirstentry + S (pfrep_left_factor_trim_equivalent) = S ((S (pfrep_position_factor_trim_equivalentfirst)) * x1)) /\ exists ff_q_pfp_factor_trim_equivalentfirstentry. x = ff_q_pfp_factor_trim_equivalentfirstentry * S ((S (pfrep_position_factor_trim_equivalentfirst)) * x1) + (pfrep_left_factor_trim_equivalent)))))) \/ (((exists pfrep_gap_factor_trim_equivalentfirstoutside. pfrep_gap_factor_trim_equivalentfirstoutside+(x2)=(pfrep_power_factor_trim_equivalent)) /\ (((pfrep_left_factor_trim_equivalent)=0))))) -> ((exists pfrep_position_factor_trim_equivalentsecond. ((pfrep_position_factor_trim_equivalentsecond+S (pfrep_power_factor_trim_equivalent)=(x9)) /\ ((((exists ff_h_pfp_factor_trim_equivalentsecondentry. ff_h_pfp_factor_trim_equivalentsecondentry + S (pfrep_right_factor_trim_equivalent) = S ((S (pfrep_position_factor_trim_equivalentsecond)) * x8)) /\ exists ff_q_pfp_factor_trim_equivalentsecondentry. x7 = ff_q_pfp_factor_trim_equivalentsecondentry * S ((S (pfrep_position_factor_trim_equivalentsecond)) * x8) + (pfrep_right_factor_trim_equivalent)))))) \/ (((exists pfrep_gap_factor_trim_equivalentsecondoutside. pfrep_gap_factor_trim_equivalentsecondoutside+(x9)=(pfrep_power_factor_trim_equivalent)) /\ (((pfrep_right_factor_trim_equivalent)=0))))) -> pfrep_left_factor_trim_equivalent=pfrep_right_factor_trim_equivalent
  60. 0060specialize prime_field_polynomial_trim_equivalent (p)
  61. 0061specialize prime_field_polynomial_trim_equivalent (x)
  62. 0062specialize prime_field_polynomial_trim_equivalent (x1)
  63. 0063specialize prime_field_polynomial_trim_equivalent (x2)
  64. 0064specialize prime_field_polynomial_trim_equivalent (x6)
  65. 0065specialize prime_field_polynomial_trim_equivalent (x7)
  66. 0066specialize prime_field_polynomial_trim_equivalent (x8)
  67. 0067specialize prime_field_polynomial_trim_equivalent (x9)
  68. 0068apply prime_field_polynomial_trim_equivalent
  69. 0069exact ht_witness_witness_witness_witness
  70. 0070have hplen : exists N. ((((x9)=0 \/ (D)=0) /\ (((N)=0)))) \/ (((~((x9)=0)) /\ (((~((D)=0)) /\ (((x9)+(D)=S (N)))))))
  71. 0071specialize polynomial_product_length_exists (x9)
  72. 0072specialize polynomial_product_length_exists (D)
  73. 0073apply polynomial_product_length_exists
  74. 0074cases hplen
  75. 0075have hpnew : exists vb vc. ((forall fom_index_pfp_factor_new_productleft. (exists fom_gap_pfp_factor_new_productleft_index_bound. fom_gap_pfp_factor_new_productleft_index_bound + S (fom_index_pfp_factor_new_productleft) = x9) -> exists fom_value_pfp_factor_new_productleft. ((((exists fom_beta_height_pfp_factor_new_productleft_entry. fom_beta_height_pfp_factor_new_productleft_entry + S (fom_value_pfp_factor_new_productleft) = S ((S (fom_index_pfp_factor_new_productleft)) * x8)) /\ exists fom_beta_quotient_pfp_factor_new_productleft_entry. x7 = fom_beta_quotient_pfp_factor_new_productleft_entry * S ((S (fom_index_pfp_factor_new_productleft)) * x8) + (fom_value_pfp_factor_new_productleft))) /\ (exists fom_gap_pfp_factor_new_productleft_value_bound. fom_gap_pfp_factor_new_productleft_value_bound + S (fom_value_pfp_factor_new_productleft) = p))) /\ (((forall fom_index_pfp_factor_new_productright. (exists fom_gap_pfp_factor_new_productright_index_bound. fom_gap_pfp_factor_new_productright_index_bound + S (fom_index_pfp_factor_new_productright) = D) -> exists fom_value_pfp_factor_new_productright. ((((exists fom_beta_height_pfp_factor_new_productright_entry. fom_beta_height_pfp_factor_new_productright_entry + S (fom_value_pfp_factor_new_productright) = S ((S (fom_index_pfp_factor_new_productright)) * dc)) /\ exists fom_beta_quotient_pfp_factor_new_productright_entry. db = fom_beta_quotient_pfp_factor_new_productright_entry * S ((S (fom_index_pfp_factor_new_productright)) * dc) + (fom_value_pfp_factor_new_productright))) /\ (exists fom_gap_pfp_factor_new_productright_value_bound. fom_gap_pfp_factor_new_productright_value_bound + S (fom_value_pfp_factor_new_productright) = p))) /\ (((((((x9)=0 \/ (D)=0) /\ (((x10)=0)))) \/ (((~((x9)=0)) /\ (((~((D)=0)) /\ (((x9)+(D)=S (x10)))))))) /\ ((forall pfc_index_factor_new_productcoefficients. (exists pfa_gap_factor_new_productcoefficientsbound. pfa_gap_factor_new_productcoefficientsbound + S (pfc_index_factor_new_productcoefficients) = (x10)) -> exists pfc_value_factor_new_productcoefficients. ((((exists ff_h_pfp_factor_new_productcoefficientsentry. ff_h_pfp_factor_new_productcoefficientsentry + S (pfc_value_factor_new_productcoefficients) = S ((S (pfc_index_factor_new_productcoefficients)) * vc)) /\ exists ff_q_pfp_factor_new_productcoefficientsentry. vb = ff_q_pfp_factor_new_productcoefficientsentry * S ((S (pfc_index_factor_new_productcoefficients)) * vc) + (pfc_value_factor_new_productcoefficients))) /\ ((exists pfc_terms_code_factor_new_productcoefficientscoefficient pfc_terms_scale_factor_new_productcoefficientscoefficient pfc_natural_sum_factor_new_productcoefficientscoefficient. ((forall pfc_index_factor_new_productcoefficientscoefficientdiagonal. (exists pfa_gap_factor_new_productcoefficientscoefficientdiagonalbound. pfa_gap_factor_new_productcoefficientscoefficientdiagonalbound + S (pfc_index_factor_new_productcoefficientscoefficientdiagonal) = (S (pfc_index_factor_new_productcoefficients))) -> exists pfc_value_factor_new_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_factor_new_productcoefficientscoefficientdiagonalentry. ff_h_pfp_factor_new_productcoefficientscoefficientdiagonalentry + S (pfc_value_factor_new_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_factor_new_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_new_productcoefficientscoefficient)) /\ exists ff_q_pfp_factor_new_productcoefficientscoefficientdiagonalentry. pfc_terms_code_factor_new_productcoefficientscoefficient = ff_q_pfp_factor_new_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_factor_new_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_new_productcoefficientscoefficient) + (pfc_value_factor_new_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_factor_new_productcoefficientscoefficientdiagonalterm pfc_left_factor_new_productcoefficientscoefficientdiagonalterm pfc_right_factor_new_productcoefficientscoefficientdiagonalterm. (((pfc_index_factor_new_productcoefficientscoefficientdiagonal)+pfc_complement_factor_new_productcoefficientscoefficientdiagonalterm=(pfc_index_factor_new_productcoefficients)) /\ ((((((exists pfa_gap_factor_new_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_factor_new_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_factor_new_productcoefficientscoefficientdiagonal) = (x9)) /\ ((((exists ff_h_pfp_factor_new_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_factor_new_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_factor_new_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_factor_new_productcoefficientscoefficientdiagonal)) * x8)) /\ exists ff_q_pfp_factor_new_productcoefficientscoefficientdiagonaltermleftentry. x7 = ff_q_pfp_factor_new_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_factor_new_productcoefficientscoefficientdiagonal)) * x8) + (pfc_left_factor_new_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_new_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_factor_new_productcoefficientscoefficientdiagonaltermleftoutside+(x9)=(pfc_index_factor_new_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_factor_new_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_factor_new_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_factor_new_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_factor_new_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_factor_new_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_factor_new_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_factor_new_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_factor_new_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_factor_new_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_factor_new_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_factor_new_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_factor_new_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_new_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_factor_new_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_factor_new_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_factor_new_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_factor_new_productcoefficientscoefficientdiagonal)=pfc_left_factor_new_productcoefficientscoefficientdiagonalterm*pfc_right_factor_new_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_factor_new_productcoefficientscoefficientsum fs_v_pfc_factor_new_productcoefficientscoefficientsum. ((((exists fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_start. fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_factor_new_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_start. fs_u_pfc_factor_new_productcoefficientscoefficientsum = fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_factor_new_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_factor_new_productcoefficientscoefficient) = S ((S (S (pfc_index_factor_new_productcoefficients))) * fs_v_pfc_factor_new_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_factor_new_productcoefficientscoefficientsum = fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_factor_new_productcoefficients))) * fs_v_pfc_factor_new_productcoefficientscoefficientsum) + (pfc_natural_sum_factor_new_productcoefficientscoefficient))) /\ forall fs_i_pfc_factor_new_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_factor_new_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_factor_new_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_factor_new_productcoefficientscoefficientsum_body_steps = S (pfc_index_factor_new_productcoefficients)) -> exists fs_a_pfc_factor_new_productcoefficientscoefficientsum_body_steps fs_r_pfc_factor_new_productcoefficientscoefficientsum_body_steps fs_s_pfc_factor_new_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_factor_new_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_new_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_new_productcoefficientscoefficient)) /\ exists fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_factor_new_productcoefficientscoefficient = fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_factor_new_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_new_productcoefficientscoefficient) + (fs_a_pfc_factor_new_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_factor_new_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_new_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_new_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_factor_new_productcoefficientscoefficientsum = fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_factor_new_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_new_productcoefficientscoefficientsum) + (fs_r_pfc_factor_new_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_factor_new_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_factor_new_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_factor_new_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_new_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_factor_new_productcoefficientscoefficientsum = fs_q_pfc_factor_new_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_factor_new_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_new_productcoefficientscoefficientsum) + (fs_s_pfc_factor_new_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_factor_new_productcoefficientscoefficientsum_body_steps = fs_r_pfc_factor_new_productcoefficientscoefficientsum_body_steps + fs_a_pfc_factor_new_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_factor_new_productcoefficientscoefficientresiduebound. pfa_gap_factor_new_productcoefficientscoefficientresiduebound + S (pfc_value_factor_new_productcoefficients) = (p)) /\ ((exists pfa_offset_left_factor_new_productcoefficientscoefficientresiduecongruence pfa_offset_right_factor_new_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_factor_new_productcoefficientscoefficient) + (p) * pfa_offset_left_factor_new_productcoefficientscoefficientresiduecongruence = (pfc_value_factor_new_productcoefficients) + (p) * pfa_offset_right_factor_new_productcoefficientscoefficientresiduecongruence))))))))))))))))))
  76. 0076specialize prime_field_polynomial_convolution_at_length_exists (p)
  77. 0077specialize prime_field_polynomial_convolution_at_length_exists (x7)
  78. 0078specialize prime_field_polynomial_convolution_at_length_exists (x8)
  79. 0079specialize prime_field_polynomial_convolution_at_length_exists (x9)
  80. 0080specialize prime_field_polynomial_convolution_at_length_exists (db)
  81. 0081specialize prime_field_polynomial_convolution_at_length_exists (dc)
  82. 0082specialize prime_field_polynomial_convolution_at_length_exists (D)
  83. 0083specialize prime_field_polynomial_convolution_at_length_exists (x10)
  84. 0084apply prime_field_polynomial_convolution_at_length_exists
  85. 0085exact hpn
  86. 0086exact htbound
  87. 0087exact hdbound
  88. 0088exact hplen_witness
  89. 0089cases hpnew
  90. 0090cases hpnew_witness
  91. 0091have hequiv : forall pfrep_power_factor_actual_equivalent pfrep_left_factor_actual_equivalent pfrep_right_factor_actual_equivalent. ((exists pfrep_position_factor_actual_equivalentfirst. ((pfrep_position_factor_actual_equivalentfirst+S (pfrep_power_factor_actual_equivalent)=(x10)) /\ ((((exists ff_h_pfp_factor_actual_equivalentfirstentry. ff_h_pfp_factor_actual_equivalentfirstentry + S (pfrep_left_factor_actual_equivalent) = S ((S (pfrep_position_factor_actual_equivalentfirst)) * x12)) /\ exists ff_q_pfp_factor_actual_equivalentfirstentry. x11 = ff_q_pfp_factor_actual_equivalentfirstentry * S ((S (pfrep_position_factor_actual_equivalentfirst)) * x12) + (pfrep_left_factor_actual_equivalent)))))) \/ (((exists pfrep_gap_factor_actual_equivalentfirstoutside. pfrep_gap_factor_actual_equivalentfirstoutside+(x10)=(pfrep_power_factor_actual_equivalent)) /\ (((pfrep_left_factor_actual_equivalent)=0))))) -> ((exists pfrep_position_factor_actual_equivalentsecond. ((pfrep_position_factor_actual_equivalentsecond+S (pfrep_power_factor_actual_equivalent)=(L)) /\ ((((exists ff_h_pfp_factor_actual_equivalentsecondentry. ff_h_pfp_factor_actual_equivalentsecondentry + S (pfrep_right_factor_actual_equivalent) = S ((S (pfrep_position_factor_actual_equivalentsecond)) * ac)) /\ exists ff_q_pfp_factor_actual_equivalentsecondentry. ab = ff_q_pfp_factor_actual_equivalentsecondentry * S ((S (pfrep_position_factor_actual_equivalentsecond)) * ac) + (pfrep_right_factor_actual_equivalent)))))) \/ (((exists pfrep_gap_factor_actual_equivalentsecondoutside. pfrep_gap_factor_actual_equivalentsecondoutside+(L)=(pfrep_power_factor_actual_equivalent)) /\ (((pfrep_right_factor_actual_equivalent)=0))))) -> pfrep_left_factor_actual_equivalent=pfrep_right_factor_actual_equivalent
  92. 0092specialize prime_field_polynomial_equivalent_transitive (x11)
  93. 0093specialize prime_field_polynomial_equivalent_transitive (x12)
  94. 0094specialize prime_field_polynomial_equivalent_transitive (x10)
  95. 0095specialize prime_field_polynomial_equivalent_transitive (x3)
  96. 0096specialize prime_field_polynomial_equivalent_transitive (x4)
  97. 0097specialize prime_field_polynomial_equivalent_transitive (x5)
  98. 0098specialize prime_field_polynomial_equivalent_transitive (ab)
  99. 0099specialize prime_field_polynomial_equivalent_transitive (ac)
  100. 0100specialize prime_field_polynomial_equivalent_transitive (L)
  101. 0101apply prime_field_polynomial_equivalent_transitive
  102. 0102specialize prime_field_polynomial_equivalent_symmetric (x3)
  103. 0103specialize prime_field_polynomial_equivalent_symmetric (x4)
  104. 0104specialize prime_field_polynomial_equivalent_symmetric (x5)
  105. 0105specialize prime_field_polynomial_equivalent_symmetric (x11)
  106. 0106specialize prime_field_polynomial_equivalent_symmetric (x12)
  107. 0107specialize prime_field_polynomial_equivalent_symmetric (x10)
  108. 0108apply prime_field_polynomial_equivalent_symmetric
  109. 0109specialize prime_field_polynomial_convolution_equivalent_congruent_left (p)
  110. 0110specialize prime_field_polynomial_convolution_equivalent_congruent_left (x)
  111. 0111specialize prime_field_polynomial_convolution_equivalent_congruent_left (x1)
  112. 0112specialize prime_field_polynomial_convolution_equivalent_congruent_left (x2)
  113. 0113specialize prime_field_polynomial_convolution_equivalent_congruent_left (db)
  114. 0114specialize prime_field_polynomial_convolution_equivalent_congruent_left (dc)
  115. 0115specialize prime_field_polynomial_convolution_equivalent_congruent_left (D)
  116. 0116specialize prime_field_polynomial_convolution_equivalent_congruent_left (x3)
  117. 0117specialize prime_field_polynomial_convolution_equivalent_congruent_left (x4)
  118. 0118specialize prime_field_polynomial_convolution_equivalent_congruent_left (x5)
  119. 0119specialize prime_field_polynomial_convolution_equivalent_congruent_left (x7)
  120. 0120specialize prime_field_polynomial_convolution_equivalent_congruent_left (x8)
  121. 0121specialize prime_field_polynomial_convolution_equivalent_congruent_left (x9)
  122. 0122specialize prime_field_polynomial_convolution_equivalent_congruent_left (x11)
  123. 0123specialize prime_field_polynomial_convolution_equivalent_congruent_left (x12)
  124. 0124specialize prime_field_polynomial_convolution_equivalent_congruent_left (x10)
  125. 0125apply prime_field_polynomial_convolution_equivalent_congruent_left
  126. 0126exact hpn
  127. 0127exact hqe
  128. 0128exact hrd_right_witness_witness_witness_witness_witness_witness_left
  129. 0129exact hpnew_witness_witness
  130. 0130exact hrd_right_witness_witness_witness_witness_witness_witness_right
  131. 0131have hn : ~(x9=0)
  132. 0132intro htzero
  133. 0133specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (p)
  134. 0134specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x7)
  135. 0135specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x8)
  136. 0136specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x9)
  137. 0137specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (db)
  138. 0138specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (dc)
  139. 0139specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (D)
  140. 0140specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x11)
  141. 0141specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x12)
  142. 0142specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x10)
  143. 0143specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (ab)
  144. 0144specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (ac)
  145. 0145specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (L)
  146. 0146specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (a)
  147. 0147apply prime_field_polynomial_product_equivalent_nonzero_left_nonempty
  148. 0148exact ha
  149. 0149exact hpnew_witness_witness
  150. 0150exact hequiv
  151. 0151exact htzero
  152. 0152have hqd : exists e. (((x9)=S (e)) /\ (((forall fom_index_pfp_factor_trim_degreecoefficients. (exists fom_gap_pfp_factor_trim_degreecoefficients_index_bound. fom_gap_pfp_factor_trim_degreecoefficients_index_bound + S (fom_index_pfp_factor_trim_degreecoefficients) = x9) -> exists fom_value_pfp_factor_trim_degreecoefficients. ((((exists fom_beta_height_pfp_factor_trim_degreecoefficients_entry. fom_beta_height_pfp_factor_trim_degreecoefficients_entry + S (fom_value_pfp_factor_trim_degreecoefficients) = S ((S (fom_index_pfp_factor_trim_degreecoefficients)) * x8)) /\ exists fom_beta_quotient_pfp_factor_trim_degreecoefficients_entry. x7 = fom_beta_quotient_pfp_factor_trim_degreecoefficients_entry * S ((S (fom_index_pfp_factor_trim_degreecoefficients)) * x8) + (fom_value_pfp_factor_trim_degreecoefficients))) /\ (exists fom_gap_pfp_factor_trim_degreecoefficients_value_bound. fom_gap_pfp_factor_trim_degreecoefficients_value_bound + S (fom_value_pfp_factor_trim_degreecoefficients) = p))) /\ ((exists pfd_leading_factor_trim_degree. ((((exists ff_h_pfp_factor_trim_degreeentry. ff_h_pfp_factor_trim_degreeentry + S (pfd_leading_factor_trim_degree) = S ((S (0)) * x8)) /\ exists ff_q_pfp_factor_trim_degreeentry. x7 = ff_q_pfp_factor_trim_degreeentry * S ((S (0)) * x8) + (pfd_leading_factor_trim_degree))) /\ ((~(pfd_leading_factor_trim_degree=0)))))))))
  153. 0153specialize prime_field_polynomial_trim_nonempty_degree_exists (p)
  154. 0154specialize prime_field_polynomial_trim_nonempty_degree_exists (x)
  155. 0155specialize prime_field_polynomial_trim_nonempty_degree_exists (x1)
  156. 0156specialize prime_field_polynomial_trim_nonempty_degree_exists (x2)
  157. 0157specialize prime_field_polynomial_trim_nonempty_degree_exists (x6)
  158. 0158specialize prime_field_polynomial_trim_nonempty_degree_exists (x7)
  159. 0159specialize prime_field_polynomial_trim_nonempty_degree_exists (x8)
  160. 0160specialize prime_field_polynomial_trim_nonempty_degree_exists (x9)
  161. 0161apply prime_field_polynomial_trim_nonempty_degree_exists
  162. 0162exact ht_witness_witness_witness_witness
  163. 0163exact hn
  164. 0164cases hqd
  165. 0165have hpd : (((x10)=S (x13+d)) /\ (((forall fom_index_pfp_factor_product_degreecoefficients. (exists fom_gap_pfp_factor_product_degreecoefficients_index_bound. fom_gap_pfp_factor_product_degreecoefficients_index_bound + S (fom_index_pfp_factor_product_degreecoefficients) = x10) -> exists fom_value_pfp_factor_product_degreecoefficients. ((((exists fom_beta_height_pfp_factor_product_degreecoefficients_entry. fom_beta_height_pfp_factor_product_degreecoefficients_entry + S (fom_value_pfp_factor_product_degreecoefficients) = S ((S (fom_index_pfp_factor_product_degreecoefficients)) * x12)) /\ exists fom_beta_quotient_pfp_factor_product_degreecoefficients_entry. x11 = fom_beta_quotient_pfp_factor_product_degreecoefficients_entry * S ((S (fom_index_pfp_factor_product_degreecoefficients)) * x12) + (fom_value_pfp_factor_product_degreecoefficients))) /\ (exists fom_gap_pfp_factor_product_degreecoefficients_value_bound. fom_gap_pfp_factor_product_degreecoefficients_value_bound + S (fom_value_pfp_factor_product_degreecoefficients) = p))) /\ ((exists pfd_leading_factor_product_degree. ((((exists ff_h_pfp_factor_product_degreeentry. ff_h_pfp_factor_product_degreeentry + S (pfd_leading_factor_product_degree) = S ((S (0)) * x12)) /\ exists ff_q_pfp_factor_product_degreeentry. x11 = ff_q_pfp_factor_product_degreeentry * S ((S (0)) * x12) + (pfd_leading_factor_product_degree))) /\ ((~(pfd_leading_factor_product_degree=0)))))))))
  166. 0166specialize prime_field_polynomial_convolution_represented_degree (p)
  167. 0167specialize prime_field_polynomial_convolution_represented_degree (x7)
  168. 0168specialize prime_field_polynomial_convolution_represented_degree (x8)
  169. 0169specialize prime_field_polynomial_convolution_represented_degree (x9)
  170. 0170specialize prime_field_polynomial_convolution_represented_degree (x13)
  171. 0171specialize prime_field_polynomial_convolution_represented_degree (db)
  172. 0172specialize prime_field_polynomial_convolution_represented_degree (dc)
  173. 0173specialize prime_field_polynomial_convolution_represented_degree (D)
  174. 0174specialize prime_field_polynomial_convolution_represented_degree (d)
  175. 0175specialize prime_field_polynomial_convolution_represented_degree (x11)
  176. 0176specialize prime_field_polynomial_convolution_represented_degree (x12)
  177. 0177specialize prime_field_polynomial_convolution_represented_degree (x10)
  178. 0178apply prime_field_polynomial_convolution_represented_degree
  179. 0179exact hp
  180. 0180exact hqd_witness
  181. 0181exact hd
  182. 0182exact hpnew_witness_witness
  183. 0183have hsum : x13+d=a
  184. 0184specialize prime_field_polynomial_equivalent_represented_degrees_equal (p)
  185. 0185specialize prime_field_polynomial_equivalent_represented_degrees_equal (x11)
  186. 0186specialize prime_field_polynomial_equivalent_represented_degrees_equal (x12)
  187. 0187specialize prime_field_polynomial_equivalent_represented_degrees_equal (x10)
  188. 0188specialize prime_field_polynomial_equivalent_represented_degrees_equal (x13+d)
  189. 0189specialize prime_field_polynomial_equivalent_represented_degrees_equal (ab)
  190. 0190specialize prime_field_polynomial_equivalent_represented_degrees_equal (ac)
  191. 0191specialize prime_field_polynomial_equivalent_represented_degrees_equal (L)
  192. 0192specialize prime_field_polynomial_equivalent_represented_degrees_equal (a)
  193. 0193apply prime_field_polynomial_equivalent_represented_degrees_equal
  194. 0194exact hpd
  195. 0195exact ha
  196. 0196exact hequiv
  197. 0197have hqlen : x9=S x13
  198. 0198cases hqd_witness
  199. 0199exact hqd_witness_left
  200. 0200have hplen2 : x10=S a
  201. 0201cases hpd
  202. 0202rewrite hpd_left
  203. 0203rewrite hsum
  204. 0204refl
  205. 0205exists x7
  206. 0206exists x8
  207. 0207exists x13
  208. 0208exists x11
  209. 0209exists x12
  210. 0210split
  211. 0211have hqdnew : (((x9)=S (x13)) /\ (((forall fom_index_pfp_factor_pack_degreecoefficients. (exists fom_gap_pfp_factor_pack_degreecoefficients_index_bound. fom_gap_pfp_factor_pack_degreecoefficients_index_bound + S (fom_index_pfp_factor_pack_degreecoefficients) = x9) -> exists fom_value_pfp_factor_pack_degreecoefficients. ((((exists fom_beta_height_pfp_factor_pack_degreecoefficients_entry. fom_beta_height_pfp_factor_pack_degreecoefficients_entry + S (fom_value_pfp_factor_pack_degreecoefficients) = S ((S (fom_index_pfp_factor_pack_degreecoefficients)) * x8)) /\ exists fom_beta_quotient_pfp_factor_pack_degreecoefficients_entry. x7 = fom_beta_quotient_pfp_factor_pack_degreecoefficients_entry * S ((S (fom_index_pfp_factor_pack_degreecoefficients)) * x8) + (fom_value_pfp_factor_pack_degreecoefficients))) /\ (exists fom_gap_pfp_factor_pack_degreecoefficients_value_bound. fom_gap_pfp_factor_pack_degreecoefficients_value_bound + S (fom_value_pfp_factor_pack_degreecoefficients) = p))) /\ ((exists pfd_leading_factor_pack_degree. ((((exists ff_h_pfp_factor_pack_degreeentry. ff_h_pfp_factor_pack_degreeentry + S (pfd_leading_factor_pack_degree) = S ((S (0)) * x8)) /\ exists ff_q_pfp_factor_pack_degreeentry. x7 = ff_q_pfp_factor_pack_degreeentry * S ((S (0)) * x8) + (pfd_leading_factor_pack_degree))) /\ ((~(pfd_leading_factor_pack_degree=0)))))))))
  212. 0212exact hqd_witness
  213. 0213rewrite hqlen at hqdnew
  214. 0214rewrite hqlen at hqdnew
  215. 0215exact hqdnew
  216. 0216split
  217. 0217have hcp : ((forall fom_index_pfp_factor_actual_newleft. (exists fom_gap_pfp_factor_actual_newleft_index_bound. fom_gap_pfp_factor_actual_newleft_index_bound + S (fom_index_pfp_factor_actual_newleft) = x9) -> exists fom_value_pfp_factor_actual_newleft. ((((exists fom_beta_height_pfp_factor_actual_newleft_entry. fom_beta_height_pfp_factor_actual_newleft_entry + S (fom_value_pfp_factor_actual_newleft) = S ((S (fom_index_pfp_factor_actual_newleft)) * x8)) /\ exists fom_beta_quotient_pfp_factor_actual_newleft_entry. x7 = fom_beta_quotient_pfp_factor_actual_newleft_entry * S ((S (fom_index_pfp_factor_actual_newleft)) * x8) + (fom_value_pfp_factor_actual_newleft))) /\ (exists fom_gap_pfp_factor_actual_newleft_value_bound. fom_gap_pfp_factor_actual_newleft_value_bound + S (fom_value_pfp_factor_actual_newleft) = p))) /\ (((forall fom_index_pfp_factor_actual_newright. (exists fom_gap_pfp_factor_actual_newright_index_bound. fom_gap_pfp_factor_actual_newright_index_bound + S (fom_index_pfp_factor_actual_newright) = D) -> exists fom_value_pfp_factor_actual_newright. ((((exists fom_beta_height_pfp_factor_actual_newright_entry. fom_beta_height_pfp_factor_actual_newright_entry + S (fom_value_pfp_factor_actual_newright) = S ((S (fom_index_pfp_factor_actual_newright)) * dc)) /\ exists fom_beta_quotient_pfp_factor_actual_newright_entry. db = fom_beta_quotient_pfp_factor_actual_newright_entry * S ((S (fom_index_pfp_factor_actual_newright)) * dc) + (fom_value_pfp_factor_actual_newright))) /\ (exists fom_gap_pfp_factor_actual_newright_value_bound. fom_gap_pfp_factor_actual_newright_value_bound + S (fom_value_pfp_factor_actual_newright) = p))) /\ (((((((x9)=0 \/ (D)=0) /\ (((x10)=0)))) \/ (((~((x9)=0)) /\ (((~((D)=0)) /\ (((x9)+(D)=S (x10)))))))) /\ ((forall pfc_index_factor_actual_newcoefficients. (exists pfa_gap_factor_actual_newcoefficientsbound. pfa_gap_factor_actual_newcoefficientsbound + S (pfc_index_factor_actual_newcoefficients) = (x10)) -> exists pfc_value_factor_actual_newcoefficients. ((((exists ff_h_pfp_factor_actual_newcoefficientsentry. ff_h_pfp_factor_actual_newcoefficientsentry + S (pfc_value_factor_actual_newcoefficients) = S ((S (pfc_index_factor_actual_newcoefficients)) * x12)) /\ exists ff_q_pfp_factor_actual_newcoefficientsentry. x11 = ff_q_pfp_factor_actual_newcoefficientsentry * S ((S (pfc_index_factor_actual_newcoefficients)) * x12) + (pfc_value_factor_actual_newcoefficients))) /\ ((exists pfc_terms_code_factor_actual_newcoefficientscoefficient pfc_terms_scale_factor_actual_newcoefficientscoefficient pfc_natural_sum_factor_actual_newcoefficientscoefficient. ((forall pfc_index_factor_actual_newcoefficientscoefficientdiagonal. (exists pfa_gap_factor_actual_newcoefficientscoefficientdiagonalbound. pfa_gap_factor_actual_newcoefficientscoefficientdiagonalbound + S (pfc_index_factor_actual_newcoefficientscoefficientdiagonal) = (S (pfc_index_factor_actual_newcoefficients))) -> exists pfc_value_factor_actual_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_factor_actual_newcoefficientscoefficientdiagonalentry. ff_h_pfp_factor_actual_newcoefficientscoefficientdiagonalentry + S (pfc_value_factor_actual_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_factor_actual_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_actual_newcoefficientscoefficient)) /\ exists ff_q_pfp_factor_actual_newcoefficientscoefficientdiagonalentry. pfc_terms_code_factor_actual_newcoefficientscoefficient = ff_q_pfp_factor_actual_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_factor_actual_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_actual_newcoefficientscoefficient) + (pfc_value_factor_actual_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_factor_actual_newcoefficientscoefficientdiagonalterm pfc_left_factor_actual_newcoefficientscoefficientdiagonalterm pfc_right_factor_actual_newcoefficientscoefficientdiagonalterm. (((pfc_index_factor_actual_newcoefficientscoefficientdiagonal)+pfc_complement_factor_actual_newcoefficientscoefficientdiagonalterm=(pfc_index_factor_actual_newcoefficients)) /\ ((((((exists pfa_gap_factor_actual_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_factor_actual_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_factor_actual_newcoefficientscoefficientdiagonal) = (x9)) /\ ((((exists ff_h_pfp_factor_actual_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_factor_actual_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_factor_actual_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_factor_actual_newcoefficientscoefficientdiagonal)) * x8)) /\ exists ff_q_pfp_factor_actual_newcoefficientscoefficientdiagonaltermleftentry. x7 = ff_q_pfp_factor_actual_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_factor_actual_newcoefficientscoefficientdiagonal)) * x8) + (pfc_left_factor_actual_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_actual_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_factor_actual_newcoefficientscoefficientdiagonaltermleftoutside+(x9)=(pfc_index_factor_actual_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_factor_actual_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_factor_actual_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_factor_actual_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_factor_actual_newcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_factor_actual_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_factor_actual_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_factor_actual_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_factor_actual_newcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_factor_actual_newcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_factor_actual_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_factor_actual_newcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_factor_actual_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_actual_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_factor_actual_newcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_factor_actual_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_factor_actual_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_factor_actual_newcoefficientscoefficientdiagonal)=pfc_left_factor_actual_newcoefficientscoefficientdiagonalterm*pfc_right_factor_actual_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_factor_actual_newcoefficientscoefficientsum fs_v_pfc_factor_actual_newcoefficientscoefficientsum. ((((exists fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_start. fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_factor_actual_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_start. fs_u_pfc_factor_actual_newcoefficientscoefficientsum = fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_factor_actual_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_factor_actual_newcoefficientscoefficient) = S ((S (S (pfc_index_factor_actual_newcoefficients))) * fs_v_pfc_factor_actual_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_factor_actual_newcoefficientscoefficientsum = fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_factor_actual_newcoefficients))) * fs_v_pfc_factor_actual_newcoefficientscoefficientsum) + (pfc_natural_sum_factor_actual_newcoefficientscoefficient))) /\ forall fs_i_pfc_factor_actual_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_factor_actual_newcoefficientscoefficientsum_body_steps = S (pfc_index_factor_actual_newcoefficients)) -> exists fs_a_pfc_factor_actual_newcoefficientscoefficientsum_body_steps fs_r_pfc_factor_actual_newcoefficientscoefficientsum_body_steps fs_s_pfc_factor_actual_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_factor_actual_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_actual_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_actual_newcoefficientscoefficient)) /\ exists fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_factor_actual_newcoefficientscoefficient = fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_factor_actual_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_actual_newcoefficientscoefficient) + (fs_a_pfc_factor_actual_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_factor_actual_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_actual_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_actual_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_factor_actual_newcoefficientscoefficientsum = fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_factor_actual_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_actual_newcoefficientscoefficientsum) + (fs_r_pfc_factor_actual_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_factor_actual_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_factor_actual_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_actual_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_factor_actual_newcoefficientscoefficientsum = fs_q_pfc_factor_actual_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_factor_actual_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_actual_newcoefficientscoefficientsum) + (fs_s_pfc_factor_actual_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_factor_actual_newcoefficientscoefficientsum_body_steps = fs_r_pfc_factor_actual_newcoefficientscoefficientsum_body_steps + fs_a_pfc_factor_actual_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_factor_actual_newcoefficientscoefficientresiduebound. pfa_gap_factor_actual_newcoefficientscoefficientresiduebound + S (pfc_value_factor_actual_newcoefficients) = (p)) /\ ((exists pfa_offset_left_factor_actual_newcoefficientscoefficientresiduecongruence pfa_offset_right_factor_actual_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_factor_actual_newcoefficientscoefficient) + (p) * pfa_offset_left_factor_actual_newcoefficientscoefficientresiduecongruence = (pfc_value_factor_actual_newcoefficients) + (p) * pfa_offset_right_factor_actual_newcoefficientscoefficientresiduecongruence))))))))))))))))))
  218. 0218exact hpnew_witness_witness
  219. 0219rewrite hqlen at hcp
  220. 0220rewrite hqlen at hcp
  221. 0221rewrite hqlen at hcp
  222. 0222rewrite hqlen at hcp
  223. 0223rewrite hqlen at hcp
  224. 0224rewrite hqlen at hcp
  225. 0225rewrite hplen2 at hcp
  226. 0226rewrite hplen2 at hcp
  227. 0227rewrite hplen2 at hcp
  228. 0228exact hcp
  229. 0229split
  230. 0230have hep : forall pfrep_power_factor_actual_equivalent pfrep_left_factor_actual_equivalent pfrep_right_factor_actual_equivalent. ((exists pfrep_position_factor_actual_equivalentfirst. ((pfrep_position_factor_actual_equivalentfirst+S (pfrep_power_factor_actual_equivalent)=(x10)) /\ ((((exists ff_h_pfp_factor_actual_equivalentfirstentry. ff_h_pfp_factor_actual_equivalentfirstentry + S (pfrep_left_factor_actual_equivalent) = S ((S (pfrep_position_factor_actual_equivalentfirst)) * x12)) /\ exists ff_q_pfp_factor_actual_equivalentfirstentry. x11 = ff_q_pfp_factor_actual_equivalentfirstentry * S ((S (pfrep_position_factor_actual_equivalentfirst)) * x12) + (pfrep_left_factor_actual_equivalent)))))) \/ (((exists pfrep_gap_factor_actual_equivalentfirstoutside. pfrep_gap_factor_actual_equivalentfirstoutside+(x10)=(pfrep_power_factor_actual_equivalent)) /\ (((pfrep_left_factor_actual_equivalent)=0))))) -> ((exists pfrep_position_factor_actual_equivalentsecond. ((pfrep_position_factor_actual_equivalentsecond+S (pfrep_power_factor_actual_equivalent)=(L)) /\ ((((exists ff_h_pfp_factor_actual_equivalentsecondentry. ff_h_pfp_factor_actual_equivalentsecondentry + S (pfrep_right_factor_actual_equivalent) = S ((S (pfrep_position_factor_actual_equivalentsecond)) * ac)) /\ exists ff_q_pfp_factor_actual_equivalentsecondentry. ab = ff_q_pfp_factor_actual_equivalentsecondentry * S ((S (pfrep_position_factor_actual_equivalentsecond)) * ac) + (pfrep_right_factor_actual_equivalent)))))) \/ (((exists pfrep_gap_factor_actual_equivalentsecondoutside. pfrep_gap_factor_actual_equivalentsecondoutside+(L)=(pfrep_power_factor_actual_equivalent)) /\ (((pfrep_right_factor_actual_equivalent)=0))))) -> pfrep_left_factor_actual_equivalent=pfrep_right_factor_actual_equivalent
  231. 0231exact hequiv
  232. 0232rewrite hplen2 at hep
  233. 0233rewrite hplen2 at hep
  234. 0234exact hep
  235. 0235exact hsum