PG0041

prime_field_polynomial_aligned_add_functional

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

Two actual aligned sums represent the same formal polynomial even when their witnesses, original output lengths, and beta codes differ.

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

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M rb rc N sb sc J. (~((p) = 1) /\ forall pfa_factor_left_aligned_function_prime pfa_factor_right_aligned_function_prime. (p) = pfa_factor_left_aligned_function_prime * pfa_factor_right_aligned_function_prime -> pfa_factor_left_aligned_function_prime = 1 \/ pfa_factor_right_aligned_function_prime = 1) -> (((forall fom_index_pfp_aligned_function_first_left_bounded. (exists fom_gap_pfp_aligned_function_first_left_bounded_index_bound. fom_gap_pfp_aligned_function_first_left_bounded_index_bound + S (fom_index_pfp_aligned_function_first_left_bounded) = L) -> exists fom_value_pfp_aligned_function_first_left_bounded. ((((exists fom_beta_height_pfp_aligned_function_first_left_bounded_entry. fom_beta_height_pfp_aligned_function_first_left_bounded_entry + S (fom_value_pfp_aligned_function_first_left_bounded) = S ((S (fom_index_pfp_aligned_function_first_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_aligned_function_first_left_bounded_entry. ab = fom_beta_quotient_pfp_aligned_function_first_left_bounded_entry * S ((S (fom_index_pfp_aligned_function_first_left_bounded)) * ac) + (fom_value_pfp_aligned_function_first_left_bounded))) /\ (exists fom_gap_pfp_aligned_function_first_left_bounded_value_bound. fom_gap_pfp_aligned_function_first_left_bounded_value_bound + S (fom_value_pfp_aligned_function_first_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_function_first_right_bounded. (exists fom_gap_pfp_aligned_function_first_right_bounded_index_bound. fom_gap_pfp_aligned_function_first_right_bounded_index_bound + S (fom_index_pfp_aligned_function_first_right_bounded) = M) -> exists fom_value_pfp_aligned_function_first_right_bounded. ((((exists fom_beta_height_pfp_aligned_function_first_right_bounded_entry. fom_beta_height_pfp_aligned_function_first_right_bounded_entry + S (fom_value_pfp_aligned_function_first_right_bounded) = S ((S (fom_index_pfp_aligned_function_first_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_aligned_function_first_right_bounded_entry. bb = fom_beta_quotient_pfp_aligned_function_first_right_bounded_entry * S ((S (fom_index_pfp_aligned_function_first_right_bounded)) * bc) + (fom_value_pfp_aligned_function_first_right_bounded))) /\ (exists fom_gap_pfp_aligned_function_first_right_bounded_value_bound. fom_gap_pfp_aligned_function_first_right_bounded_value_bound + S (fom_value_pfp_aligned_function_first_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_function_first_result_bounded. (exists fom_gap_pfp_aligned_function_first_result_bounded_index_bound. fom_gap_pfp_aligned_function_first_result_bounded_index_bound + S (fom_index_pfp_aligned_function_first_result_bounded) = N) -> exists fom_value_pfp_aligned_function_first_result_bounded. ((((exists fom_beta_height_pfp_aligned_function_first_result_bounded_entry. fom_beta_height_pfp_aligned_function_first_result_bounded_entry + S (fom_value_pfp_aligned_function_first_result_bounded) = S ((S (fom_index_pfp_aligned_function_first_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_aligned_function_first_result_bounded_entry. rb = fom_beta_quotient_pfp_aligned_function_first_result_bounded_entry * S ((S (fom_index_pfp_aligned_function_first_result_bounded)) * rc) + (fom_value_pfp_aligned_function_first_result_bounded))) /\ (exists fom_gap_pfp_aligned_function_first_result_bounded_value_bound. fom_gap_pfp_aligned_function_first_result_bounded_value_bound + S (fom_value_pfp_aligned_function_first_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_function_first pfaa_left_c_aligned_function_first pfaa_right_b_aligned_function_first pfaa_right_c_aligned_function_first pfaa_sum_b_aligned_function_first pfaa_sum_c_aligned_function_first pfaa_length_aligned_function_first. ((((forall pfrep_power_aligned_function_first_witness_common_left pfrep_left_aligned_function_first_witness_common_left pfrep_right_aligned_function_first_witness_common_left. ((exists pfrep_position_aligned_function_first_witness_common_leftfirst. ((pfrep_position_aligned_function_first_witness_common_leftfirst+S (pfrep_power_aligned_function_first_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_aligned_function_first_witness_common_leftfirstentry. ff_h_pfp_aligned_function_first_witness_common_leftfirstentry + S (pfrep_left_aligned_function_first_witness_common_left) = S ((S (pfrep_position_aligned_function_first_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_aligned_function_first_witness_common_leftfirstentry. ab = ff_q_pfp_aligned_function_first_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_function_first_witness_common_leftfirst)) * ac) + (pfrep_left_aligned_function_first_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_function_first_witness_common_leftfirstoutside. pfrep_gap_aligned_function_first_witness_common_leftfirstoutside+(L)=(pfrep_power_aligned_function_first_witness_common_left)) /\ (((pfrep_left_aligned_function_first_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_function_first_witness_common_leftsecond. ((pfrep_position_aligned_function_first_witness_common_leftsecond+S (pfrep_power_aligned_function_first_witness_common_left)=(pfaa_length_aligned_function_first)) /\ ((((exists ff_h_pfp_aligned_function_first_witness_common_leftsecondentry. ff_h_pfp_aligned_function_first_witness_common_leftsecondentry + S (pfrep_right_aligned_function_first_witness_common_left) = S ((S (pfrep_position_aligned_function_first_witness_common_leftsecond)) * pfaa_left_c_aligned_function_first)) /\ exists ff_q_pfp_aligned_function_first_witness_common_leftsecondentry. pfaa_left_b_aligned_function_first = ff_q_pfp_aligned_function_first_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_function_first_witness_common_leftsecond)) * pfaa_left_c_aligned_function_first) + (pfrep_right_aligned_function_first_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_function_first_witness_common_leftsecondoutside. pfrep_gap_aligned_function_first_witness_common_leftsecondoutside+(pfaa_length_aligned_function_first)=(pfrep_power_aligned_function_first_witness_common_left)) /\ (((pfrep_right_aligned_function_first_witness_common_left)=0))))) -> pfrep_left_aligned_function_first_witness_common_left=pfrep_right_aligned_function_first_witness_common_left) /\ ((forall pfrep_power_aligned_function_first_witness_common_right pfrep_left_aligned_function_first_witness_common_right pfrep_right_aligned_function_first_witness_common_right. ((exists pfrep_position_aligned_function_first_witness_common_rightfirst. ((pfrep_position_aligned_function_first_witness_common_rightfirst+S (pfrep_power_aligned_function_first_witness_common_right)=(M)) /\ ((((exists ff_h_pfp_aligned_function_first_witness_common_rightfirstentry. ff_h_pfp_aligned_function_first_witness_common_rightfirstentry + S (pfrep_left_aligned_function_first_witness_common_right) = S ((S (pfrep_position_aligned_function_first_witness_common_rightfirst)) * bc)) /\ exists ff_q_pfp_aligned_function_first_witness_common_rightfirstentry. bb = ff_q_pfp_aligned_function_first_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_function_first_witness_common_rightfirst)) * bc) + (pfrep_left_aligned_function_first_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_function_first_witness_common_rightfirstoutside. pfrep_gap_aligned_function_first_witness_common_rightfirstoutside+(M)=(pfrep_power_aligned_function_first_witness_common_right)) /\ (((pfrep_left_aligned_function_first_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_function_first_witness_common_rightsecond. ((pfrep_position_aligned_function_first_witness_common_rightsecond+S (pfrep_power_aligned_function_first_witness_common_right)=(pfaa_length_aligned_function_first)) /\ ((((exists ff_h_pfp_aligned_function_first_witness_common_rightsecondentry. ff_h_pfp_aligned_function_first_witness_common_rightsecondentry + S (pfrep_right_aligned_function_first_witness_common_right) = S ((S (pfrep_position_aligned_function_first_witness_common_rightsecond)) * pfaa_right_c_aligned_function_first)) /\ exists ff_q_pfp_aligned_function_first_witness_common_rightsecondentry. pfaa_right_b_aligned_function_first = ff_q_pfp_aligned_function_first_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_function_first_witness_common_rightsecond)) * pfaa_right_c_aligned_function_first) + (pfrep_right_aligned_function_first_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_function_first_witness_common_rightsecondoutside. pfrep_gap_aligned_function_first_witness_common_rightsecondoutside+(pfaa_length_aligned_function_first)=(pfrep_power_aligned_function_first_witness_common_right)) /\ (((pfrep_right_aligned_function_first_witness_common_right)=0))))) -> pfrep_left_aligned_function_first_witness_common_right=pfrep_right_aligned_function_first_witness_common_right)))) /\ (((forall pfp_index_aligned_function_first_witness_operation. (exists pfa_gap_aligned_function_first_witness_operationindex. pfa_gap_aligned_function_first_witness_operationindex + S (pfp_index_aligned_function_first_witness_operation) = (pfaa_length_aligned_function_first)) -> exists pfp_left_aligned_function_first_witness_operation pfp_right_aligned_function_first_witness_operation pfp_value_aligned_function_first_witness_operation. ((((exists ff_h_pfp_aligned_function_first_witness_operationleft. ff_h_pfp_aligned_function_first_witness_operationleft + S (pfp_left_aligned_function_first_witness_operation) = S ((S (pfp_index_aligned_function_first_witness_operation)) * pfaa_left_c_aligned_function_first)) /\ exists ff_q_pfp_aligned_function_first_witness_operationleft. pfaa_left_b_aligned_function_first = ff_q_pfp_aligned_function_first_witness_operationleft * S ((S (pfp_index_aligned_function_first_witness_operation)) * pfaa_left_c_aligned_function_first) + (pfp_left_aligned_function_first_witness_operation))) /\ (((((exists ff_h_pfp_aligned_function_first_witness_operationright. ff_h_pfp_aligned_function_first_witness_operationright + S (pfp_right_aligned_function_first_witness_operation) = S ((S (pfp_index_aligned_function_first_witness_operation)) * pfaa_right_c_aligned_function_first)) /\ exists ff_q_pfp_aligned_function_first_witness_operationright. pfaa_right_b_aligned_function_first = ff_q_pfp_aligned_function_first_witness_operationright * S ((S (pfp_index_aligned_function_first_witness_operation)) * pfaa_right_c_aligned_function_first) + (pfp_right_aligned_function_first_witness_operation))) /\ (((((exists ff_h_pfp_aligned_function_first_witness_operationtarget. ff_h_pfp_aligned_function_first_witness_operationtarget + S (pfp_value_aligned_function_first_witness_operation) = S ((S (pfp_index_aligned_function_first_witness_operation)) * pfaa_sum_c_aligned_function_first)) /\ exists ff_q_pfp_aligned_function_first_witness_operationtarget. pfaa_sum_b_aligned_function_first = ff_q_pfp_aligned_function_first_witness_operationtarget * S ((S (pfp_index_aligned_function_first_witness_operation)) * pfaa_sum_c_aligned_function_first) + (pfp_value_aligned_function_first_witness_operation))) /\ ((((exists pfa_gap_aligned_function_first_witness_operationoperationleft. pfa_gap_aligned_function_first_witness_operationoperationleft + S (pfp_left_aligned_function_first_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_function_first_witness_operationoperationright. pfa_gap_aligned_function_first_witness_operationoperationright + S (pfp_right_aligned_function_first_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_function_first_witness_operationoperationresultbound. pfa_gap_aligned_function_first_witness_operationoperationresultbound + S (pfp_value_aligned_function_first_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_function_first_witness_operationoperationresultcongruence pfa_offset_right_aligned_function_first_witness_operationoperationresultcongruence. ((pfp_left_aligned_function_first_witness_operation) + (pfp_right_aligned_function_first_witness_operation)) + (p) * pfa_offset_left_aligned_function_first_witness_operationoperationresultcongruence = (pfp_value_aligned_function_first_witness_operation) + (p) * pfa_offset_right_aligned_function_first_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_function_first_witness_output pfrep_left_aligned_function_first_witness_output pfrep_right_aligned_function_first_witness_output. ((exists pfrep_position_aligned_function_first_witness_outputfirst. ((pfrep_position_aligned_function_first_witness_outputfirst+S (pfrep_power_aligned_function_first_witness_output)=(pfaa_length_aligned_function_first)) /\ ((((exists ff_h_pfp_aligned_function_first_witness_outputfirstentry. ff_h_pfp_aligned_function_first_witness_outputfirstentry + S (pfrep_left_aligned_function_first_witness_output) = S ((S (pfrep_position_aligned_function_first_witness_outputfirst)) * pfaa_sum_c_aligned_function_first)) /\ exists ff_q_pfp_aligned_function_first_witness_outputfirstentry. pfaa_sum_b_aligned_function_first = ff_q_pfp_aligned_function_first_witness_outputfirstentry * S ((S (pfrep_position_aligned_function_first_witness_outputfirst)) * pfaa_sum_c_aligned_function_first) + (pfrep_left_aligned_function_first_witness_output)))))) \/ (((exists pfrep_gap_aligned_function_first_witness_outputfirstoutside. pfrep_gap_aligned_function_first_witness_outputfirstoutside+(pfaa_length_aligned_function_first)=(pfrep_power_aligned_function_first_witness_output)) /\ (((pfrep_left_aligned_function_first_witness_output)=0))))) -> ((exists pfrep_position_aligned_function_first_witness_outputsecond. ((pfrep_position_aligned_function_first_witness_outputsecond+S (pfrep_power_aligned_function_first_witness_output)=(N)) /\ ((((exists ff_h_pfp_aligned_function_first_witness_outputsecondentry. ff_h_pfp_aligned_function_first_witness_outputsecondentry + S (pfrep_right_aligned_function_first_witness_output) = S ((S (pfrep_position_aligned_function_first_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_aligned_function_first_witness_outputsecondentry. rb = ff_q_pfp_aligned_function_first_witness_outputsecondentry * S ((S (pfrep_position_aligned_function_first_witness_outputsecond)) * rc) + (pfrep_right_aligned_function_first_witness_output)))))) \/ (((exists pfrep_gap_aligned_function_first_witness_outputsecondoutside. pfrep_gap_aligned_function_first_witness_outputsecondoutside+(N)=(pfrep_power_aligned_function_first_witness_output)) /\ (((pfrep_right_aligned_function_first_witness_output)=0))))) -> pfrep_left_aligned_function_first_witness_output=pfrep_right_aligned_function_first_witness_output))))))))))))) -> (((forall fom_index_pfp_aligned_function_second_left_bounded. (exists fom_gap_pfp_aligned_function_second_left_bounded_index_bound. fom_gap_pfp_aligned_function_second_left_bounded_index_bound + S (fom_index_pfp_aligned_function_second_left_bounded) = L) -> exists fom_value_pfp_aligned_function_second_left_bounded. ((((exists fom_beta_height_pfp_aligned_function_second_left_bounded_entry. fom_beta_height_pfp_aligned_function_second_left_bounded_entry + S (fom_value_pfp_aligned_function_second_left_bounded) = S ((S (fom_index_pfp_aligned_function_second_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_aligned_function_second_left_bounded_entry. ab = fom_beta_quotient_pfp_aligned_function_second_left_bounded_entry * S ((S (fom_index_pfp_aligned_function_second_left_bounded)) * ac) + (fom_value_pfp_aligned_function_second_left_bounded))) /\ (exists fom_gap_pfp_aligned_function_second_left_bounded_value_bound. fom_gap_pfp_aligned_function_second_left_bounded_value_bound + S (fom_value_pfp_aligned_function_second_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_function_second_right_bounded. (exists fom_gap_pfp_aligned_function_second_right_bounded_index_bound. fom_gap_pfp_aligned_function_second_right_bounded_index_bound + S (fom_index_pfp_aligned_function_second_right_bounded) = M) -> exists fom_value_pfp_aligned_function_second_right_bounded. ((((exists fom_beta_height_pfp_aligned_function_second_right_bounded_entry. fom_beta_height_pfp_aligned_function_second_right_bounded_entry + S (fom_value_pfp_aligned_function_second_right_bounded) = S ((S (fom_index_pfp_aligned_function_second_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_aligned_function_second_right_bounded_entry. bb = fom_beta_quotient_pfp_aligned_function_second_right_bounded_entry * S ((S (fom_index_pfp_aligned_function_second_right_bounded)) * bc) + (fom_value_pfp_aligned_function_second_right_bounded))) /\ (exists fom_gap_pfp_aligned_function_second_right_bounded_value_bound. fom_gap_pfp_aligned_function_second_right_bounded_value_bound + S (fom_value_pfp_aligned_function_second_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_function_second_result_bounded. (exists fom_gap_pfp_aligned_function_second_result_bounded_index_bound. fom_gap_pfp_aligned_function_second_result_bounded_index_bound + S (fom_index_pfp_aligned_function_second_result_bounded) = J) -> exists fom_value_pfp_aligned_function_second_result_bounded. ((((exists fom_beta_height_pfp_aligned_function_second_result_bounded_entry. fom_beta_height_pfp_aligned_function_second_result_bounded_entry + S (fom_value_pfp_aligned_function_second_result_bounded) = S ((S (fom_index_pfp_aligned_function_second_result_bounded)) * sc)) /\ exists fom_beta_quotient_pfp_aligned_function_second_result_bounded_entry. sb = fom_beta_quotient_pfp_aligned_function_second_result_bounded_entry * S ((S (fom_index_pfp_aligned_function_second_result_bounded)) * sc) + (fom_value_pfp_aligned_function_second_result_bounded))) /\ (exists fom_gap_pfp_aligned_function_second_result_bounded_value_bound. fom_gap_pfp_aligned_function_second_result_bounded_value_bound + S (fom_value_pfp_aligned_function_second_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_function_second pfaa_left_c_aligned_function_second pfaa_right_b_aligned_function_second pfaa_right_c_aligned_function_second pfaa_sum_b_aligned_function_second pfaa_sum_c_aligned_function_second pfaa_length_aligned_function_second. ((((forall pfrep_power_aligned_function_second_witness_common_left pfrep_left_aligned_function_second_witness_common_left pfrep_right_aligned_function_second_witness_common_left. ((exists pfrep_position_aligned_function_second_witness_common_leftfirst. ((pfrep_position_aligned_function_second_witness_common_leftfirst+S (pfrep_power_aligned_function_second_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_aligned_function_second_witness_common_leftfirstentry. ff_h_pfp_aligned_function_second_witness_common_leftfirstentry + S (pfrep_left_aligned_function_second_witness_common_left) = S ((S (pfrep_position_aligned_function_second_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_aligned_function_second_witness_common_leftfirstentry. ab = ff_q_pfp_aligned_function_second_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_function_second_witness_common_leftfirst)) * ac) + (pfrep_left_aligned_function_second_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_function_second_witness_common_leftfirstoutside. pfrep_gap_aligned_function_second_witness_common_leftfirstoutside+(L)=(pfrep_power_aligned_function_second_witness_common_left)) /\ (((pfrep_left_aligned_function_second_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_function_second_witness_common_leftsecond. ((pfrep_position_aligned_function_second_witness_common_leftsecond+S (pfrep_power_aligned_function_second_witness_common_left)=(pfaa_length_aligned_function_second)) /\ ((((exists ff_h_pfp_aligned_function_second_witness_common_leftsecondentry. ff_h_pfp_aligned_function_second_witness_common_leftsecondentry + S (pfrep_right_aligned_function_second_witness_common_left) = S ((S (pfrep_position_aligned_function_second_witness_common_leftsecond)) * pfaa_left_c_aligned_function_second)) /\ exists ff_q_pfp_aligned_function_second_witness_common_leftsecondentry. pfaa_left_b_aligned_function_second = ff_q_pfp_aligned_function_second_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_function_second_witness_common_leftsecond)) * pfaa_left_c_aligned_function_second) + (pfrep_right_aligned_function_second_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_function_second_witness_common_leftsecondoutside. pfrep_gap_aligned_function_second_witness_common_leftsecondoutside+(pfaa_length_aligned_function_second)=(pfrep_power_aligned_function_second_witness_common_left)) /\ (((pfrep_right_aligned_function_second_witness_common_left)=0))))) -> pfrep_left_aligned_function_second_witness_common_left=pfrep_right_aligned_function_second_witness_common_left) /\ ((forall pfrep_power_aligned_function_second_witness_common_right pfrep_left_aligned_function_second_witness_common_right pfrep_right_aligned_function_second_witness_common_right. ((exists pfrep_position_aligned_function_second_witness_common_rightfirst. ((pfrep_position_aligned_function_second_witness_common_rightfirst+S (pfrep_power_aligned_function_second_witness_common_right)=(M)) /\ ((((exists ff_h_pfp_aligned_function_second_witness_common_rightfirstentry. ff_h_pfp_aligned_function_second_witness_common_rightfirstentry + S (pfrep_left_aligned_function_second_witness_common_right) = S ((S (pfrep_position_aligned_function_second_witness_common_rightfirst)) * bc)) /\ exists ff_q_pfp_aligned_function_second_witness_common_rightfirstentry. bb = ff_q_pfp_aligned_function_second_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_function_second_witness_common_rightfirst)) * bc) + (pfrep_left_aligned_function_second_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_function_second_witness_common_rightfirstoutside. pfrep_gap_aligned_function_second_witness_common_rightfirstoutside+(M)=(pfrep_power_aligned_function_second_witness_common_right)) /\ (((pfrep_left_aligned_function_second_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_function_second_witness_common_rightsecond. ((pfrep_position_aligned_function_second_witness_common_rightsecond+S (pfrep_power_aligned_function_second_witness_common_right)=(pfaa_length_aligned_function_second)) /\ ((((exists ff_h_pfp_aligned_function_second_witness_common_rightsecondentry. ff_h_pfp_aligned_function_second_witness_common_rightsecondentry + S (pfrep_right_aligned_function_second_witness_common_right) = S ((S (pfrep_position_aligned_function_second_witness_common_rightsecond)) * pfaa_right_c_aligned_function_second)) /\ exists ff_q_pfp_aligned_function_second_witness_common_rightsecondentry. pfaa_right_b_aligned_function_second = ff_q_pfp_aligned_function_second_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_function_second_witness_common_rightsecond)) * pfaa_right_c_aligned_function_second) + (pfrep_right_aligned_function_second_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_function_second_witness_common_rightsecondoutside. pfrep_gap_aligned_function_second_witness_common_rightsecondoutside+(pfaa_length_aligned_function_second)=(pfrep_power_aligned_function_second_witness_common_right)) /\ (((pfrep_right_aligned_function_second_witness_common_right)=0))))) -> pfrep_left_aligned_function_second_witness_common_right=pfrep_right_aligned_function_second_witness_common_right)))) /\ (((forall pfp_index_aligned_function_second_witness_operation. (exists pfa_gap_aligned_function_second_witness_operationindex. pfa_gap_aligned_function_second_witness_operationindex + S (pfp_index_aligned_function_second_witness_operation) = (pfaa_length_aligned_function_second)) -> exists pfp_left_aligned_function_second_witness_operation pfp_right_aligned_function_second_witness_operation pfp_value_aligned_function_second_witness_operation. ((((exists ff_h_pfp_aligned_function_second_witness_operationleft. ff_h_pfp_aligned_function_second_witness_operationleft + S (pfp_left_aligned_function_second_witness_operation) = S ((S (pfp_index_aligned_function_second_witness_operation)) * pfaa_left_c_aligned_function_second)) /\ exists ff_q_pfp_aligned_function_second_witness_operationleft. pfaa_left_b_aligned_function_second = ff_q_pfp_aligned_function_second_witness_operationleft * S ((S (pfp_index_aligned_function_second_witness_operation)) * pfaa_left_c_aligned_function_second) + (pfp_left_aligned_function_second_witness_operation))) /\ (((((exists ff_h_pfp_aligned_function_second_witness_operationright. ff_h_pfp_aligned_function_second_witness_operationright + S (pfp_right_aligned_function_second_witness_operation) = S ((S (pfp_index_aligned_function_second_witness_operation)) * pfaa_right_c_aligned_function_second)) /\ exists ff_q_pfp_aligned_function_second_witness_operationright. pfaa_right_b_aligned_function_second = ff_q_pfp_aligned_function_second_witness_operationright * S ((S (pfp_index_aligned_function_second_witness_operation)) * pfaa_right_c_aligned_function_second) + (pfp_right_aligned_function_second_witness_operation))) /\ (((((exists ff_h_pfp_aligned_function_second_witness_operationtarget. ff_h_pfp_aligned_function_second_witness_operationtarget + S (pfp_value_aligned_function_second_witness_operation) = S ((S (pfp_index_aligned_function_second_witness_operation)) * pfaa_sum_c_aligned_function_second)) /\ exists ff_q_pfp_aligned_function_second_witness_operationtarget. pfaa_sum_b_aligned_function_second = ff_q_pfp_aligned_function_second_witness_operationtarget * S ((S (pfp_index_aligned_function_second_witness_operation)) * pfaa_sum_c_aligned_function_second) + (pfp_value_aligned_function_second_witness_operation))) /\ ((((exists pfa_gap_aligned_function_second_witness_operationoperationleft. pfa_gap_aligned_function_second_witness_operationoperationleft + S (pfp_left_aligned_function_second_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_function_second_witness_operationoperationright. pfa_gap_aligned_function_second_witness_operationoperationright + S (pfp_right_aligned_function_second_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_function_second_witness_operationoperationresultbound. pfa_gap_aligned_function_second_witness_operationoperationresultbound + S (pfp_value_aligned_function_second_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_function_second_witness_operationoperationresultcongruence pfa_offset_right_aligned_function_second_witness_operationoperationresultcongruence. ((pfp_left_aligned_function_second_witness_operation) + (pfp_right_aligned_function_second_witness_operation)) + (p) * pfa_offset_left_aligned_function_second_witness_operationoperationresultcongruence = (pfp_value_aligned_function_second_witness_operation) + (p) * pfa_offset_right_aligned_function_second_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_function_second_witness_output pfrep_left_aligned_function_second_witness_output pfrep_right_aligned_function_second_witness_output. ((exists pfrep_position_aligned_function_second_witness_outputfirst. ((pfrep_position_aligned_function_second_witness_outputfirst+S (pfrep_power_aligned_function_second_witness_output)=(pfaa_length_aligned_function_second)) /\ ((((exists ff_h_pfp_aligned_function_second_witness_outputfirstentry. ff_h_pfp_aligned_function_second_witness_outputfirstentry + S (pfrep_left_aligned_function_second_witness_output) = S ((S (pfrep_position_aligned_function_second_witness_outputfirst)) * pfaa_sum_c_aligned_function_second)) /\ exists ff_q_pfp_aligned_function_second_witness_outputfirstentry. pfaa_sum_b_aligned_function_second = ff_q_pfp_aligned_function_second_witness_outputfirstentry * S ((S (pfrep_position_aligned_function_second_witness_outputfirst)) * pfaa_sum_c_aligned_function_second) + (pfrep_left_aligned_function_second_witness_output)))))) \/ (((exists pfrep_gap_aligned_function_second_witness_outputfirstoutside. pfrep_gap_aligned_function_second_witness_outputfirstoutside+(pfaa_length_aligned_function_second)=(pfrep_power_aligned_function_second_witness_output)) /\ (((pfrep_left_aligned_function_second_witness_output)=0))))) -> ((exists pfrep_position_aligned_function_second_witness_outputsecond. ((pfrep_position_aligned_function_second_witness_outputsecond+S (pfrep_power_aligned_function_second_witness_output)=(J)) /\ ((((exists ff_h_pfp_aligned_function_second_witness_outputsecondentry. ff_h_pfp_aligned_function_second_witness_outputsecondentry + S (pfrep_right_aligned_function_second_witness_output) = S ((S (pfrep_position_aligned_function_second_witness_outputsecond)) * sc)) /\ exists ff_q_pfp_aligned_function_second_witness_outputsecondentry. sb = ff_q_pfp_aligned_function_second_witness_outputsecondentry * S ((S (pfrep_position_aligned_function_second_witness_outputsecond)) * sc) + (pfrep_right_aligned_function_second_witness_output)))))) \/ (((exists pfrep_gap_aligned_function_second_witness_outputsecondoutside. pfrep_gap_aligned_function_second_witness_outputsecondoutside+(J)=(pfrep_power_aligned_function_second_witness_output)) /\ (((pfrep_right_aligned_function_second_witness_output)=0))))) -> pfrep_left_aligned_function_second_witness_output=pfrep_right_aligned_function_second_witness_output))))))))))))) -> (forall pfrep_power_aligned_function_result pfrep_left_aligned_function_result pfrep_right_aligned_function_result. ((exists pfrep_position_aligned_function_resultfirst. ((pfrep_position_aligned_function_resultfirst+S (pfrep_power_aligned_function_result)=(N)) /\ ((((exists ff_h_pfp_aligned_function_resultfirstentry. ff_h_pfp_aligned_function_resultfirstentry + S (pfrep_left_aligned_function_result) = S ((S (pfrep_position_aligned_function_resultfirst)) * rc)) /\ exists ff_q_pfp_aligned_function_resultfirstentry. rb = ff_q_pfp_aligned_function_resultfirstentry * S ((S (pfrep_position_aligned_function_resultfirst)) * rc) + (pfrep_left_aligned_function_result)))))) \/ (((exists pfrep_gap_aligned_function_resultfirstoutside. pfrep_gap_aligned_function_resultfirstoutside+(N)=(pfrep_power_aligned_function_result)) /\ (((pfrep_left_aligned_function_result)=0))))) -> ((exists pfrep_position_aligned_function_resultsecond. ((pfrep_position_aligned_function_resultsecond+S (pfrep_power_aligned_function_result)=(J)) /\ ((((exists ff_h_pfp_aligned_function_resultsecondentry. ff_h_pfp_aligned_function_resultsecondentry + S (pfrep_right_aligned_function_result) = S ((S (pfrep_position_aligned_function_resultsecond)) * sc)) /\ exists ff_q_pfp_aligned_function_resultsecondentry. sb = ff_q_pfp_aligned_function_resultsecondentry * S ((S (pfrep_position_aligned_function_resultsecond)) * sc) + (pfrep_right_aligned_function_result)))))) \/ (((exists pfrep_gap_aligned_function_resultsecondoutside. pfrep_gap_aligned_function_resultsecondoutside+(J)=(pfrep_power_aligned_function_result)) /\ (((pfrep_right_aligned_function_result)=0))))) -> pfrep_left_aligned_function_result=pfrep_right_aligned_function_result)

Constructive proof overview

Generated structural guide

Two actual aligned sums represent the same formal polynomial even when their witnesses, original output lengths, and beta codes differ.

The unchanged tactic script uses 4 declared prerequisites and contains 117 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PG003A prime_field_polynomial_common_representatives_functional prime_field_polynomial_add_equivalent_congruent Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_symmetric Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_transitive Alpha theorem; checked-use authorized

Direct dependents

PG0043 prime_field_polynomial_aligned_add_realize PG0058 prime_field_polynomial_right_divides_aligned_add

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

117 script commands · 15 reading checkpoints · 4 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 (1)
prime field polynomial common representatives functional

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

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro rb
  9. L9
    intro rc
  10. L10
    intro N
02Fix variables and assumptionsL11–16

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

  1. L11
    intro sb
  2. L12
    intro sc
  3. L13
    intro J
  4. L14
    intro hp
  5. L15
    intro hr
  6. L16
    intro hs
03Separate the logical casesL17–26

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

  1. L17
    cases hr
  2. L18
    cases hr_right
  3. L19
    cases hr_right_right
  4. L20
    cases hr_right_right_right
  5. L21
    cases hr_right_right_right_witness
  6. L22
    cases hr_right_right_right_witness_witness
  7. L23
    cases hr_right_right_right_witness_witness_witness
  8. L24
    cases hr_right_right_right_witness_witness_witness_witness
  9. L25
    cases hr_right_right_right_witness_witness_witness_witness_witness
  10. L26
    cases hr_right_right_right_witness_witness_witness_witness_witness_witness
04Separate the logical casesL27–36

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

  1. L27
    cases hr_right_right_right_witness_witness_witness_witness_witness_witness_witness
  2. L28
    cases hr_right_right_right_witness_witness_witness_witness_witness_witness_witness_right
  3. L29
    cases hs
  4. L30
    cases hs_right
  5. L31
    cases hs_right_right
  6. L32
    cases hs_right_right_right
  7. L33
    cases hs_right_right_right_witness
  8. L34
    cases hs_right_right_right_witness_witness
  9. L35
    cases hs_right_right_right_witness_witness_witness
  10. L36
    cases hs_right_right_right_witness_witness_witness_witness
05Separate the logical casesL37–40

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

  1. L37
    cases hs_right_right_right_witness_witness_witness_witness_witness
  2. L38
    cases hs_right_right_right_witness_witness_witness_witness_witness_witness
  3. L39
    cases hs_right_right_right_witness_witness_witness_witness_witness_witness_witness
  4. L40
    cases hs_right_right_right_witness_witness_witness_witness_witness_witness_witness_right
06Establish hcL41–50

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

  1. L41
    have hc : CommonRepresentatives(x,x1,x6,x2,x3,x6,x7,x8,x9,x10,x13)Definitions: CommonRepresentatives
  2. L42
    specialize prime_field_polynomial_common_representatives_functional (ab)
  3. L43
    specialize prime_field_polynomial_common_representatives_functional (ac)
  4. L44
    specialize prime_field_polynomial_common_representatives_functional (L)
  5. L45
    specialize prime_field_polynomial_common_representatives_functional (bb)
  6. L46
    specialize prime_field_polynomial_common_representatives_functional (bc)
  7. L47
    specialize prime_field_polynomial_common_representatives_functional (M)
  8. L48
    specialize prime_field_polynomial_common_representatives_functional (x)
  9. L49
    specialize prime_field_polynomial_common_representatives_functional (x1)
  10. L50
    specialize prime_field_polynomial_common_representatives_functional (x2)
07Use earlier factsL51–60

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

  1. L51
    specialize prime_field_polynomial_common_representatives_functional (x3)
  2. L52
    specialize prime_field_polynomial_common_representatives_functional (x6)
  3. L53
    specialize prime_field_polynomial_common_representatives_functional (x7)
  4. L54
    specialize prime_field_polynomial_common_representatives_functional (x8)
  5. L55
    specialize prime_field_polynomial_common_representatives_functional (x9)
  6. L56
    specialize prime_field_polynomial_common_representatives_functional (x10)
  7. L57
    specialize prime_field_polynomial_common_representatives_functional (x13)
  8. L58
    apply prime_field_polynomial_common_representatives_functional
  9. L59
    exact hr_right_right_right_witness_witness_witness_witness_witness_witness_witness_left
  10. L60
    exact hs_right_right_right_witness_witness_witness_witness_witness_witness_witness_left
08Separate the logical casesL61–61

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

  1. L61
    cases hc
09Establish hmL62–71

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

  1. L62
    have hm : PolynomialEquivalent(x4,x5,x6,x11,x12,x13)Definitions: PolynomialEquivalent
  2. L63
    specialize prime_field_polynomial_add_equivalent_congruent (p)
  3. L64
    specialize prime_field_polynomial_add_equivalent_congruent (x)
  4. L65
    specialize prime_field_polynomial_add_equivalent_congruent (x1)
  5. L66
    specialize prime_field_polynomial_add_equivalent_congruent (x2)
  6. L67
    specialize prime_field_polynomial_add_equivalent_congruent (x3)
  7. L68
    specialize prime_field_polynomial_add_equivalent_congruent (x4)
  8. L69
    specialize prime_field_polynomial_add_equivalent_congruent (x5)
  9. L70
    specialize prime_field_polynomial_add_equivalent_congruent (x6)
  10. L71
    specialize prime_field_polynomial_add_equivalent_congruent (x7)
10Use earlier factsL72–81

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

  1. L72
    specialize prime_field_polynomial_add_equivalent_congruent (x8)
  2. L73
    specialize prime_field_polynomial_add_equivalent_congruent (x9)
  3. L74
    specialize prime_field_polynomial_add_equivalent_congruent (x10)
  4. L75
    specialize prime_field_polynomial_add_equivalent_congruent (x11)
  5. L76
    specialize prime_field_polynomial_add_equivalent_congruent (x12)
  6. L77
    specialize prime_field_polynomial_add_equivalent_congruent (x13)
  7. L78
    apply prime_field_polynomial_add_equivalent_congruent
  8. L79
    exact hp
  9. L80
    exact hc_left
  10. L81
    exact hc_right
11Use earlier factsL82–83

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

  1. L82
    exact hr_right_right_right_witness_witness_witness_witness_witness_witness_witness_right_left
  2. L83
    exact hs_right_right_right_witness_witness_witness_witness_witness_witness_witness_right_left
12Establish hreverseL84–92

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

  1. L84
    have hreverse : PolynomialEquivalent(rb,rc,N,x4,x5,x6)Definitions: PolynomialEquivalent
  2. L85
    specialize prime_field_polynomial_equivalent_symmetric (x4)
  3. L86
    specialize prime_field_polynomial_equivalent_symmetric (x5)
  4. L87
    specialize prime_field_polynomial_equivalent_symmetric (x6)
  5. L88
    specialize prime_field_polynomial_equivalent_symmetric (rb)
  6. L89
    specialize prime_field_polynomial_equivalent_symmetric (rc)
  7. L90
    specialize prime_field_polynomial_equivalent_symmetric (N)
  8. L91
    apply prime_field_polynomial_equivalent_symmetric
  9. L92
    exact hr_right_right_right_witness_witness_witness_witness_witness_witness_witness_right_right
13Establish hmiddleL93–102

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

  1. L93
    have hmiddle : PolynomialEquivalent(rb,rc,N,x11,x12,x13)Definitions: PolynomialEquivalent
  2. L94
    specialize prime_field_polynomial_equivalent_transitive (rb)
  3. L95
    specialize prime_field_polynomial_equivalent_transitive (rc)
  4. L96
    specialize prime_field_polynomial_equivalent_transitive (N)
  5. L97
    specialize prime_field_polynomial_equivalent_transitive (x4)
  6. L98
    specialize prime_field_polynomial_equivalent_transitive (x5)
  7. L99
    specialize prime_field_polynomial_equivalent_transitive (x6)
  8. L100
    specialize prime_field_polynomial_equivalent_transitive (x11)
  9. L101
    specialize prime_field_polynomial_equivalent_transitive (x12)
  10. L102
    specialize prime_field_polynomial_equivalent_transitive (x13)
14Use earlier factsL103–112

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

  1. L103
    apply prime_field_polynomial_equivalent_transitive
  2. L104
    exact hreverse
  3. L105
    exact hm
  4. L106
    specialize prime_field_polynomial_equivalent_transitive (rb)
  5. L107
    specialize prime_field_polynomial_equivalent_transitive (rc)
  6. L108
    specialize prime_field_polynomial_equivalent_transitive (N)
  7. L109
    specialize prime_field_polynomial_equivalent_transitive (x11)
  8. L110
    specialize prime_field_polynomial_equivalent_transitive (x12)
  9. L111
    specialize prime_field_polynomial_equivalent_transitive (x13)
  10. L112
    specialize prime_field_polynomial_equivalent_transitive (sb)
15Use earlier factsL113–117

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

  1. L113
    specialize prime_field_polynomial_equivalent_transitive (sc)
  2. L114
    specialize prime_field_polynomial_equivalent_transitive (J)
  3. L115
    apply prime_field_polynomial_equivalent_transitive
  4. L116
    exact hmiddle
  5. L117
    exact hs_right_right_right_witness_witness_witness_witness_witness_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 117 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro rb
  9. 0009intro rc
  10. 0010intro N
  11. 0011intro sb
  12. 0012intro sc
  13. 0013intro J
  14. 0014intro hp
  15. 0015intro hr
  16. 0016intro hs
  17. 0017cases hr
  18. 0018cases hr_right
  19. 0019cases hr_right_right
  20. 0020cases hr_right_right_right
  21. 0021cases hr_right_right_right_witness
  22. 0022cases hr_right_right_right_witness_witness
  23. 0023cases hr_right_right_right_witness_witness_witness
  24. 0024cases hr_right_right_right_witness_witness_witness_witness
  25. 0025cases hr_right_right_right_witness_witness_witness_witness_witness
  26. 0026cases hr_right_right_right_witness_witness_witness_witness_witness_witness
  27. 0027cases hr_right_right_right_witness_witness_witness_witness_witness_witness_witness
  28. 0028cases hr_right_right_right_witness_witness_witness_witness_witness_witness_witness_right
  29. 0029cases hs
  30. 0030cases hs_right
  31. 0031cases hs_right_right
  32. 0032cases hs_right_right_right
  33. 0033cases hs_right_right_right_witness
  34. 0034cases hs_right_right_right_witness_witness
  35. 0035cases hs_right_right_right_witness_witness_witness
  36. 0036cases hs_right_right_right_witness_witness_witness_witness
  37. 0037cases hs_right_right_right_witness_witness_witness_witness_witness
  38. 0038cases hs_right_right_right_witness_witness_witness_witness_witness_witness
  39. 0039cases hs_right_right_right_witness_witness_witness_witness_witness_witness_witness
  40. 0040cases hs_right_right_right_witness_witness_witness_witness_witness_witness_witness_right
  41. 0041have hc : ((forall pfrep_power_aligned_function_left pfrep_left_aligned_function_left pfrep_right_aligned_function_left. ((exists pfrep_position_aligned_function_leftfirst. ((pfrep_position_aligned_function_leftfirst+S (pfrep_power_aligned_function_left)=(x6)) /\ ((((exists ff_h_pfp_aligned_function_leftfirstentry. ff_h_pfp_aligned_function_leftfirstentry + S (pfrep_left_aligned_function_left) = S ((S (pfrep_position_aligned_function_leftfirst)) * x1)) /\ exists ff_q_pfp_aligned_function_leftfirstentry. x = ff_q_pfp_aligned_function_leftfirstentry * S ((S (pfrep_position_aligned_function_leftfirst)) * x1) + (pfrep_left_aligned_function_left)))))) \/ (((exists pfrep_gap_aligned_function_leftfirstoutside. pfrep_gap_aligned_function_leftfirstoutside+(x6)=(pfrep_power_aligned_function_left)) /\ (((pfrep_left_aligned_function_left)=0))))) -> ((exists pfrep_position_aligned_function_leftsecond. ((pfrep_position_aligned_function_leftsecond+S (pfrep_power_aligned_function_left)=(x13)) /\ ((((exists ff_h_pfp_aligned_function_leftsecondentry. ff_h_pfp_aligned_function_leftsecondentry + S (pfrep_right_aligned_function_left) = S ((S (pfrep_position_aligned_function_leftsecond)) * x8)) /\ exists ff_q_pfp_aligned_function_leftsecondentry. x7 = ff_q_pfp_aligned_function_leftsecondentry * S ((S (pfrep_position_aligned_function_leftsecond)) * x8) + (pfrep_right_aligned_function_left)))))) \/ (((exists pfrep_gap_aligned_function_leftsecondoutside. pfrep_gap_aligned_function_leftsecondoutside+(x13)=(pfrep_power_aligned_function_left)) /\ (((pfrep_right_aligned_function_left)=0))))) -> pfrep_left_aligned_function_left=pfrep_right_aligned_function_left) /\ ((forall pfrep_power_aligned_function_right pfrep_left_aligned_function_right pfrep_right_aligned_function_right. ((exists pfrep_position_aligned_function_rightfirst. ((pfrep_position_aligned_function_rightfirst+S (pfrep_power_aligned_function_right)=(x6)) /\ ((((exists ff_h_pfp_aligned_function_rightfirstentry. ff_h_pfp_aligned_function_rightfirstentry + S (pfrep_left_aligned_function_right) = S ((S (pfrep_position_aligned_function_rightfirst)) * x3)) /\ exists ff_q_pfp_aligned_function_rightfirstentry. x2 = ff_q_pfp_aligned_function_rightfirstentry * S ((S (pfrep_position_aligned_function_rightfirst)) * x3) + (pfrep_left_aligned_function_right)))))) \/ (((exists pfrep_gap_aligned_function_rightfirstoutside. pfrep_gap_aligned_function_rightfirstoutside+(x6)=(pfrep_power_aligned_function_right)) /\ (((pfrep_left_aligned_function_right)=0))))) -> ((exists pfrep_position_aligned_function_rightsecond. ((pfrep_position_aligned_function_rightsecond+S (pfrep_power_aligned_function_right)=(x13)) /\ ((((exists ff_h_pfp_aligned_function_rightsecondentry. ff_h_pfp_aligned_function_rightsecondentry + S (pfrep_right_aligned_function_right) = S ((S (pfrep_position_aligned_function_rightsecond)) * x10)) /\ exists ff_q_pfp_aligned_function_rightsecondentry. x9 = ff_q_pfp_aligned_function_rightsecondentry * S ((S (pfrep_position_aligned_function_rightsecond)) * x10) + (pfrep_right_aligned_function_right)))))) \/ (((exists pfrep_gap_aligned_function_rightsecondoutside. pfrep_gap_aligned_function_rightsecondoutside+(x13)=(pfrep_power_aligned_function_right)) /\ (((pfrep_right_aligned_function_right)=0))))) -> pfrep_left_aligned_function_right=pfrep_right_aligned_function_right)))
  42. 0042specialize prime_field_polynomial_common_representatives_functional (ab)
  43. 0043specialize prime_field_polynomial_common_representatives_functional (ac)
  44. 0044specialize prime_field_polynomial_common_representatives_functional (L)
  45. 0045specialize prime_field_polynomial_common_representatives_functional (bb)
  46. 0046specialize prime_field_polynomial_common_representatives_functional (bc)
  47. 0047specialize prime_field_polynomial_common_representatives_functional (M)
  48. 0048specialize prime_field_polynomial_common_representatives_functional (x)
  49. 0049specialize prime_field_polynomial_common_representatives_functional (x1)
  50. 0050specialize prime_field_polynomial_common_representatives_functional (x2)
  51. 0051specialize prime_field_polynomial_common_representatives_functional (x3)
  52. 0052specialize prime_field_polynomial_common_representatives_functional (x6)
  53. 0053specialize prime_field_polynomial_common_representatives_functional (x7)
  54. 0054specialize prime_field_polynomial_common_representatives_functional (x8)
  55. 0055specialize prime_field_polynomial_common_representatives_functional (x9)
  56. 0056specialize prime_field_polynomial_common_representatives_functional (x10)
  57. 0057specialize prime_field_polynomial_common_representatives_functional (x13)
  58. 0058apply prime_field_polynomial_common_representatives_functional
  59. 0059exact hr_right_right_right_witness_witness_witness_witness_witness_witness_witness_left
  60. 0060exact hs_right_right_right_witness_witness_witness_witness_witness_witness_witness_left
  61. 0061cases hc
  62. 0062have hm : forall pfrep_power_aligned_function_sums pfrep_left_aligned_function_sums pfrep_right_aligned_function_sums. ((exists pfrep_position_aligned_function_sumsfirst. ((pfrep_position_aligned_function_sumsfirst+S (pfrep_power_aligned_function_sums)=(x6)) /\ ((((exists ff_h_pfp_aligned_function_sumsfirstentry. ff_h_pfp_aligned_function_sumsfirstentry + S (pfrep_left_aligned_function_sums) = S ((S (pfrep_position_aligned_function_sumsfirst)) * x5)) /\ exists ff_q_pfp_aligned_function_sumsfirstentry. x4 = ff_q_pfp_aligned_function_sumsfirstentry * S ((S (pfrep_position_aligned_function_sumsfirst)) * x5) + (pfrep_left_aligned_function_sums)))))) \/ (((exists pfrep_gap_aligned_function_sumsfirstoutside. pfrep_gap_aligned_function_sumsfirstoutside+(x6)=(pfrep_power_aligned_function_sums)) /\ (((pfrep_left_aligned_function_sums)=0))))) -> ((exists pfrep_position_aligned_function_sumssecond. ((pfrep_position_aligned_function_sumssecond+S (pfrep_power_aligned_function_sums)=(x13)) /\ ((((exists ff_h_pfp_aligned_function_sumssecondentry. ff_h_pfp_aligned_function_sumssecondentry + S (pfrep_right_aligned_function_sums) = S ((S (pfrep_position_aligned_function_sumssecond)) * x12)) /\ exists ff_q_pfp_aligned_function_sumssecondentry. x11 = ff_q_pfp_aligned_function_sumssecondentry * S ((S (pfrep_position_aligned_function_sumssecond)) * x12) + (pfrep_right_aligned_function_sums)))))) \/ (((exists pfrep_gap_aligned_function_sumssecondoutside. pfrep_gap_aligned_function_sumssecondoutside+(x13)=(pfrep_power_aligned_function_sums)) /\ (((pfrep_right_aligned_function_sums)=0))))) -> pfrep_left_aligned_function_sums=pfrep_right_aligned_function_sums
  63. 0063specialize prime_field_polynomial_add_equivalent_congruent (p)
  64. 0064specialize prime_field_polynomial_add_equivalent_congruent (x)
  65. 0065specialize prime_field_polynomial_add_equivalent_congruent (x1)
  66. 0066specialize prime_field_polynomial_add_equivalent_congruent (x2)
  67. 0067specialize prime_field_polynomial_add_equivalent_congruent (x3)
  68. 0068specialize prime_field_polynomial_add_equivalent_congruent (x4)
  69. 0069specialize prime_field_polynomial_add_equivalent_congruent (x5)
  70. 0070specialize prime_field_polynomial_add_equivalent_congruent (x6)
  71. 0071specialize prime_field_polynomial_add_equivalent_congruent (x7)
  72. 0072specialize prime_field_polynomial_add_equivalent_congruent (x8)
  73. 0073specialize prime_field_polynomial_add_equivalent_congruent (x9)
  74. 0074specialize prime_field_polynomial_add_equivalent_congruent (x10)
  75. 0075specialize prime_field_polynomial_add_equivalent_congruent (x11)
  76. 0076specialize prime_field_polynomial_add_equivalent_congruent (x12)
  77. 0077specialize prime_field_polynomial_add_equivalent_congruent (x13)
  78. 0078apply prime_field_polynomial_add_equivalent_congruent
  79. 0079exact hp
  80. 0080exact hc_left
  81. 0081exact hc_right
  82. 0082exact hr_right_right_right_witness_witness_witness_witness_witness_witness_witness_right_left
  83. 0083exact hs_right_right_right_witness_witness_witness_witness_witness_witness_witness_right_left
  84. 0084have hreverse : forall pfrep_power_aligned_function_reverse pfrep_left_aligned_function_reverse pfrep_right_aligned_function_reverse. ((exists pfrep_position_aligned_function_reversefirst. ((pfrep_position_aligned_function_reversefirst+S (pfrep_power_aligned_function_reverse)=(N)) /\ ((((exists ff_h_pfp_aligned_function_reversefirstentry. ff_h_pfp_aligned_function_reversefirstentry + S (pfrep_left_aligned_function_reverse) = S ((S (pfrep_position_aligned_function_reversefirst)) * rc)) /\ exists ff_q_pfp_aligned_function_reversefirstentry. rb = ff_q_pfp_aligned_function_reversefirstentry * S ((S (pfrep_position_aligned_function_reversefirst)) * rc) + (pfrep_left_aligned_function_reverse)))))) \/ (((exists pfrep_gap_aligned_function_reversefirstoutside. pfrep_gap_aligned_function_reversefirstoutside+(N)=(pfrep_power_aligned_function_reverse)) /\ (((pfrep_left_aligned_function_reverse)=0))))) -> ((exists pfrep_position_aligned_function_reversesecond. ((pfrep_position_aligned_function_reversesecond+S (pfrep_power_aligned_function_reverse)=(x6)) /\ ((((exists ff_h_pfp_aligned_function_reversesecondentry. ff_h_pfp_aligned_function_reversesecondentry + S (pfrep_right_aligned_function_reverse) = S ((S (pfrep_position_aligned_function_reversesecond)) * x5)) /\ exists ff_q_pfp_aligned_function_reversesecondentry. x4 = ff_q_pfp_aligned_function_reversesecondentry * S ((S (pfrep_position_aligned_function_reversesecond)) * x5) + (pfrep_right_aligned_function_reverse)))))) \/ (((exists pfrep_gap_aligned_function_reversesecondoutside. pfrep_gap_aligned_function_reversesecondoutside+(x6)=(pfrep_power_aligned_function_reverse)) /\ (((pfrep_right_aligned_function_reverse)=0))))) -> pfrep_left_aligned_function_reverse=pfrep_right_aligned_function_reverse
  85. 0085specialize prime_field_polynomial_equivalent_symmetric (x4)
  86. 0086specialize prime_field_polynomial_equivalent_symmetric (x5)
  87. 0087specialize prime_field_polynomial_equivalent_symmetric (x6)
  88. 0088specialize prime_field_polynomial_equivalent_symmetric (rb)
  89. 0089specialize prime_field_polynomial_equivalent_symmetric (rc)
  90. 0090specialize prime_field_polynomial_equivalent_symmetric (N)
  91. 0091apply prime_field_polynomial_equivalent_symmetric
  92. 0092exact hr_right_right_right_witness_witness_witness_witness_witness_witness_witness_right_right
  93. 0093have hmiddle : forall pfrep_power_aligned_function_middle pfrep_left_aligned_function_middle pfrep_right_aligned_function_middle. ((exists pfrep_position_aligned_function_middlefirst. ((pfrep_position_aligned_function_middlefirst+S (pfrep_power_aligned_function_middle)=(N)) /\ ((((exists ff_h_pfp_aligned_function_middlefirstentry. ff_h_pfp_aligned_function_middlefirstentry + S (pfrep_left_aligned_function_middle) = S ((S (pfrep_position_aligned_function_middlefirst)) * rc)) /\ exists ff_q_pfp_aligned_function_middlefirstentry. rb = ff_q_pfp_aligned_function_middlefirstentry * S ((S (pfrep_position_aligned_function_middlefirst)) * rc) + (pfrep_left_aligned_function_middle)))))) \/ (((exists pfrep_gap_aligned_function_middlefirstoutside. pfrep_gap_aligned_function_middlefirstoutside+(N)=(pfrep_power_aligned_function_middle)) /\ (((pfrep_left_aligned_function_middle)=0))))) -> ((exists pfrep_position_aligned_function_middlesecond. ((pfrep_position_aligned_function_middlesecond+S (pfrep_power_aligned_function_middle)=(x13)) /\ ((((exists ff_h_pfp_aligned_function_middlesecondentry. ff_h_pfp_aligned_function_middlesecondentry + S (pfrep_right_aligned_function_middle) = S ((S (pfrep_position_aligned_function_middlesecond)) * x12)) /\ exists ff_q_pfp_aligned_function_middlesecondentry. x11 = ff_q_pfp_aligned_function_middlesecondentry * S ((S (pfrep_position_aligned_function_middlesecond)) * x12) + (pfrep_right_aligned_function_middle)))))) \/ (((exists pfrep_gap_aligned_function_middlesecondoutside. pfrep_gap_aligned_function_middlesecondoutside+(x13)=(pfrep_power_aligned_function_middle)) /\ (((pfrep_right_aligned_function_middle)=0))))) -> pfrep_left_aligned_function_middle=pfrep_right_aligned_function_middle
  94. 0094specialize prime_field_polynomial_equivalent_transitive (rb)
  95. 0095specialize prime_field_polynomial_equivalent_transitive (rc)
  96. 0096specialize prime_field_polynomial_equivalent_transitive (N)
  97. 0097specialize prime_field_polynomial_equivalent_transitive (x4)
  98. 0098specialize prime_field_polynomial_equivalent_transitive (x5)
  99. 0099specialize prime_field_polynomial_equivalent_transitive (x6)
  100. 0100specialize prime_field_polynomial_equivalent_transitive (x11)
  101. 0101specialize prime_field_polynomial_equivalent_transitive (x12)
  102. 0102specialize prime_field_polynomial_equivalent_transitive (x13)
  103. 0103apply prime_field_polynomial_equivalent_transitive
  104. 0104exact hreverse
  105. 0105exact hm
  106. 0106specialize prime_field_polynomial_equivalent_transitive (rb)
  107. 0107specialize prime_field_polynomial_equivalent_transitive (rc)
  108. 0108specialize prime_field_polynomial_equivalent_transitive (N)
  109. 0109specialize prime_field_polynomial_equivalent_transitive (x11)
  110. 0110specialize prime_field_polynomial_equivalent_transitive (x12)
  111. 0111specialize prime_field_polynomial_equivalent_transitive (x13)
  112. 0112specialize prime_field_polynomial_equivalent_transitive (sb)
  113. 0113specialize prime_field_polynomial_equivalent_transitive (sc)
  114. 0114specialize prime_field_polynomial_equivalent_transitive (J)
  115. 0115apply prime_field_polynomial_equivalent_transitive
  116. 0116exact hmiddle
  117. 0117exact hs_right_right_right_witness_witness_witness_witness_witness_witness_witness_right_right