PG0043

prime_field_polynomial_aligned_add_realize

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

Realize the addition on any supplied canonical equal-length representatives: construct a sum, prove formal output uniqueness, then transport the actual operation by decoded coefficient equality.

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 ub uc vb vc tb tc K. (~((p) = 1) /\ forall pfa_factor_left_realize_prime pfa_factor_right_realize_prime. (p) = pfa_factor_left_realize_prime * pfa_factor_right_realize_prime -> pfa_factor_left_realize_prime = 1 \/ pfa_factor_right_realize_prime = 1) -> (((forall fom_index_pfp_realize_original_left_bounded. (exists fom_gap_pfp_realize_original_left_bounded_index_bound. fom_gap_pfp_realize_original_left_bounded_index_bound + S (fom_index_pfp_realize_original_left_bounded) = L) -> exists fom_value_pfp_realize_original_left_bounded. ((((exists fom_beta_height_pfp_realize_original_left_bounded_entry. fom_beta_height_pfp_realize_original_left_bounded_entry + S (fom_value_pfp_realize_original_left_bounded) = S ((S (fom_index_pfp_realize_original_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_realize_original_left_bounded_entry. ab = fom_beta_quotient_pfp_realize_original_left_bounded_entry * S ((S (fom_index_pfp_realize_original_left_bounded)) * ac) + (fom_value_pfp_realize_original_left_bounded))) /\ (exists fom_gap_pfp_realize_original_left_bounded_value_bound. fom_gap_pfp_realize_original_left_bounded_value_bound + S (fom_value_pfp_realize_original_left_bounded) = p))) /\ (((forall fom_index_pfp_realize_original_right_bounded. (exists fom_gap_pfp_realize_original_right_bounded_index_bound. fom_gap_pfp_realize_original_right_bounded_index_bound + S (fom_index_pfp_realize_original_right_bounded) = M) -> exists fom_value_pfp_realize_original_right_bounded. ((((exists fom_beta_height_pfp_realize_original_right_bounded_entry. fom_beta_height_pfp_realize_original_right_bounded_entry + S (fom_value_pfp_realize_original_right_bounded) = S ((S (fom_index_pfp_realize_original_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_realize_original_right_bounded_entry. bb = fom_beta_quotient_pfp_realize_original_right_bounded_entry * S ((S (fom_index_pfp_realize_original_right_bounded)) * bc) + (fom_value_pfp_realize_original_right_bounded))) /\ (exists fom_gap_pfp_realize_original_right_bounded_value_bound. fom_gap_pfp_realize_original_right_bounded_value_bound + S (fom_value_pfp_realize_original_right_bounded) = p))) /\ (((forall fom_index_pfp_realize_original_result_bounded. (exists fom_gap_pfp_realize_original_result_bounded_index_bound. fom_gap_pfp_realize_original_result_bounded_index_bound + S (fom_index_pfp_realize_original_result_bounded) = N) -> exists fom_value_pfp_realize_original_result_bounded. ((((exists fom_beta_height_pfp_realize_original_result_bounded_entry. fom_beta_height_pfp_realize_original_result_bounded_entry + S (fom_value_pfp_realize_original_result_bounded) = S ((S (fom_index_pfp_realize_original_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_realize_original_result_bounded_entry. rb = fom_beta_quotient_pfp_realize_original_result_bounded_entry * S ((S (fom_index_pfp_realize_original_result_bounded)) * rc) + (fom_value_pfp_realize_original_result_bounded))) /\ (exists fom_gap_pfp_realize_original_result_bounded_value_bound. fom_gap_pfp_realize_original_result_bounded_value_bound + S (fom_value_pfp_realize_original_result_bounded) = p))) /\ ((exists pfaa_left_b_realize_original pfaa_left_c_realize_original pfaa_right_b_realize_original pfaa_right_c_realize_original pfaa_sum_b_realize_original pfaa_sum_c_realize_original pfaa_length_realize_original. ((((forall pfrep_power_realize_original_witness_common_left pfrep_left_realize_original_witness_common_left pfrep_right_realize_original_witness_common_left. ((exists pfrep_position_realize_original_witness_common_leftfirst. ((pfrep_position_realize_original_witness_common_leftfirst+S (pfrep_power_realize_original_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_realize_original_witness_common_leftfirstentry. ff_h_pfp_realize_original_witness_common_leftfirstentry + S (pfrep_left_realize_original_witness_common_left) = S ((S (pfrep_position_realize_original_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_realize_original_witness_common_leftfirstentry. ab = ff_q_pfp_realize_original_witness_common_leftfirstentry * S ((S (pfrep_position_realize_original_witness_common_leftfirst)) * ac) + (pfrep_left_realize_original_witness_common_left)))))) \/ (((exists pfrep_gap_realize_original_witness_common_leftfirstoutside. pfrep_gap_realize_original_witness_common_leftfirstoutside+(L)=(pfrep_power_realize_original_witness_common_left)) /\ (((pfrep_left_realize_original_witness_common_left)=0))))) -> ((exists pfrep_position_realize_original_witness_common_leftsecond. ((pfrep_position_realize_original_witness_common_leftsecond+S (pfrep_power_realize_original_witness_common_left)=(pfaa_length_realize_original)) /\ ((((exists ff_h_pfp_realize_original_witness_common_leftsecondentry. ff_h_pfp_realize_original_witness_common_leftsecondentry + S (pfrep_right_realize_original_witness_common_left) = S ((S (pfrep_position_realize_original_witness_common_leftsecond)) * pfaa_left_c_realize_original)) /\ exists ff_q_pfp_realize_original_witness_common_leftsecondentry. pfaa_left_b_realize_original = ff_q_pfp_realize_original_witness_common_leftsecondentry * S ((S (pfrep_position_realize_original_witness_common_leftsecond)) * pfaa_left_c_realize_original) + (pfrep_right_realize_original_witness_common_left)))))) \/ (((exists pfrep_gap_realize_original_witness_common_leftsecondoutside. pfrep_gap_realize_original_witness_common_leftsecondoutside+(pfaa_length_realize_original)=(pfrep_power_realize_original_witness_common_left)) /\ (((pfrep_right_realize_original_witness_common_left)=0))))) -> pfrep_left_realize_original_witness_common_left=pfrep_right_realize_original_witness_common_left) /\ ((forall pfrep_power_realize_original_witness_common_right pfrep_left_realize_original_witness_common_right pfrep_right_realize_original_witness_common_right. ((exists pfrep_position_realize_original_witness_common_rightfirst. ((pfrep_position_realize_original_witness_common_rightfirst+S (pfrep_power_realize_original_witness_common_right)=(M)) /\ ((((exists ff_h_pfp_realize_original_witness_common_rightfirstentry. ff_h_pfp_realize_original_witness_common_rightfirstentry + S (pfrep_left_realize_original_witness_common_right) = S ((S (pfrep_position_realize_original_witness_common_rightfirst)) * bc)) /\ exists ff_q_pfp_realize_original_witness_common_rightfirstentry. bb = ff_q_pfp_realize_original_witness_common_rightfirstentry * S ((S (pfrep_position_realize_original_witness_common_rightfirst)) * bc) + (pfrep_left_realize_original_witness_common_right)))))) \/ (((exists pfrep_gap_realize_original_witness_common_rightfirstoutside. pfrep_gap_realize_original_witness_common_rightfirstoutside+(M)=(pfrep_power_realize_original_witness_common_right)) /\ (((pfrep_left_realize_original_witness_common_right)=0))))) -> ((exists pfrep_position_realize_original_witness_common_rightsecond. ((pfrep_position_realize_original_witness_common_rightsecond+S (pfrep_power_realize_original_witness_common_right)=(pfaa_length_realize_original)) /\ ((((exists ff_h_pfp_realize_original_witness_common_rightsecondentry. ff_h_pfp_realize_original_witness_common_rightsecondentry + S (pfrep_right_realize_original_witness_common_right) = S ((S (pfrep_position_realize_original_witness_common_rightsecond)) * pfaa_right_c_realize_original)) /\ exists ff_q_pfp_realize_original_witness_common_rightsecondentry. pfaa_right_b_realize_original = ff_q_pfp_realize_original_witness_common_rightsecondentry * S ((S (pfrep_position_realize_original_witness_common_rightsecond)) * pfaa_right_c_realize_original) + (pfrep_right_realize_original_witness_common_right)))))) \/ (((exists pfrep_gap_realize_original_witness_common_rightsecondoutside. pfrep_gap_realize_original_witness_common_rightsecondoutside+(pfaa_length_realize_original)=(pfrep_power_realize_original_witness_common_right)) /\ (((pfrep_right_realize_original_witness_common_right)=0))))) -> pfrep_left_realize_original_witness_common_right=pfrep_right_realize_original_witness_common_right)))) /\ (((forall pfp_index_realize_original_witness_operation. (exists pfa_gap_realize_original_witness_operationindex. pfa_gap_realize_original_witness_operationindex + S (pfp_index_realize_original_witness_operation) = (pfaa_length_realize_original)) -> exists pfp_left_realize_original_witness_operation pfp_right_realize_original_witness_operation pfp_value_realize_original_witness_operation. ((((exists ff_h_pfp_realize_original_witness_operationleft. ff_h_pfp_realize_original_witness_operationleft + S (pfp_left_realize_original_witness_operation) = S ((S (pfp_index_realize_original_witness_operation)) * pfaa_left_c_realize_original)) /\ exists ff_q_pfp_realize_original_witness_operationleft. pfaa_left_b_realize_original = ff_q_pfp_realize_original_witness_operationleft * S ((S (pfp_index_realize_original_witness_operation)) * pfaa_left_c_realize_original) + (pfp_left_realize_original_witness_operation))) /\ (((((exists ff_h_pfp_realize_original_witness_operationright. ff_h_pfp_realize_original_witness_operationright + S (pfp_right_realize_original_witness_operation) = S ((S (pfp_index_realize_original_witness_operation)) * pfaa_right_c_realize_original)) /\ exists ff_q_pfp_realize_original_witness_operationright. pfaa_right_b_realize_original = ff_q_pfp_realize_original_witness_operationright * S ((S (pfp_index_realize_original_witness_operation)) * pfaa_right_c_realize_original) + (pfp_right_realize_original_witness_operation))) /\ (((((exists ff_h_pfp_realize_original_witness_operationtarget. ff_h_pfp_realize_original_witness_operationtarget + S (pfp_value_realize_original_witness_operation) = S ((S (pfp_index_realize_original_witness_operation)) * pfaa_sum_c_realize_original)) /\ exists ff_q_pfp_realize_original_witness_operationtarget. pfaa_sum_b_realize_original = ff_q_pfp_realize_original_witness_operationtarget * S ((S (pfp_index_realize_original_witness_operation)) * pfaa_sum_c_realize_original) + (pfp_value_realize_original_witness_operation))) /\ ((((exists pfa_gap_realize_original_witness_operationoperationleft. pfa_gap_realize_original_witness_operationoperationleft + S (pfp_left_realize_original_witness_operation) = (p)) /\ (((exists pfa_gap_realize_original_witness_operationoperationright. pfa_gap_realize_original_witness_operationoperationright + S (pfp_right_realize_original_witness_operation) = (p)) /\ ((((exists pfa_gap_realize_original_witness_operationoperationresultbound. pfa_gap_realize_original_witness_operationoperationresultbound + S (pfp_value_realize_original_witness_operation) = (p)) /\ ((exists pfa_offset_left_realize_original_witness_operationoperationresultcongruence pfa_offset_right_realize_original_witness_operationoperationresultcongruence. ((pfp_left_realize_original_witness_operation) + (pfp_right_realize_original_witness_operation)) + (p) * pfa_offset_left_realize_original_witness_operationoperationresultcongruence = (pfp_value_realize_original_witness_operation) + (p) * pfa_offset_right_realize_original_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_realize_original_witness_output pfrep_left_realize_original_witness_output pfrep_right_realize_original_witness_output. ((exists pfrep_position_realize_original_witness_outputfirst. ((pfrep_position_realize_original_witness_outputfirst+S (pfrep_power_realize_original_witness_output)=(pfaa_length_realize_original)) /\ ((((exists ff_h_pfp_realize_original_witness_outputfirstentry. ff_h_pfp_realize_original_witness_outputfirstentry + S (pfrep_left_realize_original_witness_output) = S ((S (pfrep_position_realize_original_witness_outputfirst)) * pfaa_sum_c_realize_original)) /\ exists ff_q_pfp_realize_original_witness_outputfirstentry. pfaa_sum_b_realize_original = ff_q_pfp_realize_original_witness_outputfirstentry * S ((S (pfrep_position_realize_original_witness_outputfirst)) * pfaa_sum_c_realize_original) + (pfrep_left_realize_original_witness_output)))))) \/ (((exists pfrep_gap_realize_original_witness_outputfirstoutside. pfrep_gap_realize_original_witness_outputfirstoutside+(pfaa_length_realize_original)=(pfrep_power_realize_original_witness_output)) /\ (((pfrep_left_realize_original_witness_output)=0))))) -> ((exists pfrep_position_realize_original_witness_outputsecond. ((pfrep_position_realize_original_witness_outputsecond+S (pfrep_power_realize_original_witness_output)=(N)) /\ ((((exists ff_h_pfp_realize_original_witness_outputsecondentry. ff_h_pfp_realize_original_witness_outputsecondentry + S (pfrep_right_realize_original_witness_output) = S ((S (pfrep_position_realize_original_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_realize_original_witness_outputsecondentry. rb = ff_q_pfp_realize_original_witness_outputsecondentry * S ((S (pfrep_position_realize_original_witness_outputsecond)) * rc) + (pfrep_right_realize_original_witness_output)))))) \/ (((exists pfrep_gap_realize_original_witness_outputsecondoutside. pfrep_gap_realize_original_witness_outputsecondoutside+(N)=(pfrep_power_realize_original_witness_output)) /\ (((pfrep_right_realize_original_witness_output)=0))))) -> pfrep_left_realize_original_witness_output=pfrep_right_realize_original_witness_output))))))))))))) -> (forall fom_index_pfp_realize_bound_0. (exists fom_gap_pfp_realize_bound_0_index_bound. fom_gap_pfp_realize_bound_0_index_bound + S (fom_index_pfp_realize_bound_0) = K) -> exists fom_value_pfp_realize_bound_0. ((((exists fom_beta_height_pfp_realize_bound_0_entry. fom_beta_height_pfp_realize_bound_0_entry + S (fom_value_pfp_realize_bound_0) = S ((S (fom_index_pfp_realize_bound_0)) * uc)) /\ exists fom_beta_quotient_pfp_realize_bound_0_entry. ub = fom_beta_quotient_pfp_realize_bound_0_entry * S ((S (fom_index_pfp_realize_bound_0)) * uc) + (fom_value_pfp_realize_bound_0))) /\ (exists fom_gap_pfp_realize_bound_0_value_bound. fom_gap_pfp_realize_bound_0_value_bound + S (fom_value_pfp_realize_bound_0) = p))) -> (forall fom_index_pfp_realize_bound_1. (exists fom_gap_pfp_realize_bound_1_index_bound. fom_gap_pfp_realize_bound_1_index_bound + S (fom_index_pfp_realize_bound_1) = K) -> exists fom_value_pfp_realize_bound_1. ((((exists fom_beta_height_pfp_realize_bound_1_entry. fom_beta_height_pfp_realize_bound_1_entry + S (fom_value_pfp_realize_bound_1) = S ((S (fom_index_pfp_realize_bound_1)) * vc)) /\ exists fom_beta_quotient_pfp_realize_bound_1_entry. vb = fom_beta_quotient_pfp_realize_bound_1_entry * S ((S (fom_index_pfp_realize_bound_1)) * vc) + (fom_value_pfp_realize_bound_1))) /\ (exists fom_gap_pfp_realize_bound_1_value_bound. fom_gap_pfp_realize_bound_1_value_bound + S (fom_value_pfp_realize_bound_1) = p))) -> (forall fom_index_pfp_realize_bound_2. (exists fom_gap_pfp_realize_bound_2_index_bound. fom_gap_pfp_realize_bound_2_index_bound + S (fom_index_pfp_realize_bound_2) = K) -> exists fom_value_pfp_realize_bound_2. ((((exists fom_beta_height_pfp_realize_bound_2_entry. fom_beta_height_pfp_realize_bound_2_entry + S (fom_value_pfp_realize_bound_2) = S ((S (fom_index_pfp_realize_bound_2)) * tc)) /\ exists fom_beta_quotient_pfp_realize_bound_2_entry. tb = fom_beta_quotient_pfp_realize_bound_2_entry * S ((S (fom_index_pfp_realize_bound_2)) * tc) + (fom_value_pfp_realize_bound_2))) /\ (exists fom_gap_pfp_realize_bound_2_value_bound. fom_gap_pfp_realize_bound_2_value_bound + S (fom_value_pfp_realize_bound_2) = p))) -> (((forall pfrep_power_realize_common_left pfrep_left_realize_common_left pfrep_right_realize_common_left. ((exists pfrep_position_realize_common_leftfirst. ((pfrep_position_realize_common_leftfirst+S (pfrep_power_realize_common_left)=(L)) /\ ((((exists ff_h_pfp_realize_common_leftfirstentry. ff_h_pfp_realize_common_leftfirstentry + S (pfrep_left_realize_common_left) = S ((S (pfrep_position_realize_common_leftfirst)) * ac)) /\ exists ff_q_pfp_realize_common_leftfirstentry. ab = ff_q_pfp_realize_common_leftfirstentry * S ((S (pfrep_position_realize_common_leftfirst)) * ac) + (pfrep_left_realize_common_left)))))) \/ (((exists pfrep_gap_realize_common_leftfirstoutside. pfrep_gap_realize_common_leftfirstoutside+(L)=(pfrep_power_realize_common_left)) /\ (((pfrep_left_realize_common_left)=0))))) -> ((exists pfrep_position_realize_common_leftsecond. ((pfrep_position_realize_common_leftsecond+S (pfrep_power_realize_common_left)=(K)) /\ ((((exists ff_h_pfp_realize_common_leftsecondentry. ff_h_pfp_realize_common_leftsecondentry + S (pfrep_right_realize_common_left) = S ((S (pfrep_position_realize_common_leftsecond)) * uc)) /\ exists ff_q_pfp_realize_common_leftsecondentry. ub = ff_q_pfp_realize_common_leftsecondentry * S ((S (pfrep_position_realize_common_leftsecond)) * uc) + (pfrep_right_realize_common_left)))))) \/ (((exists pfrep_gap_realize_common_leftsecondoutside. pfrep_gap_realize_common_leftsecondoutside+(K)=(pfrep_power_realize_common_left)) /\ (((pfrep_right_realize_common_left)=0))))) -> pfrep_left_realize_common_left=pfrep_right_realize_common_left) /\ ((forall pfrep_power_realize_common_right pfrep_left_realize_common_right pfrep_right_realize_common_right. ((exists pfrep_position_realize_common_rightfirst. ((pfrep_position_realize_common_rightfirst+S (pfrep_power_realize_common_right)=(M)) /\ ((((exists ff_h_pfp_realize_common_rightfirstentry. ff_h_pfp_realize_common_rightfirstentry + S (pfrep_left_realize_common_right) = S ((S (pfrep_position_realize_common_rightfirst)) * bc)) /\ exists ff_q_pfp_realize_common_rightfirstentry. bb = ff_q_pfp_realize_common_rightfirstentry * S ((S (pfrep_position_realize_common_rightfirst)) * bc) + (pfrep_left_realize_common_right)))))) \/ (((exists pfrep_gap_realize_common_rightfirstoutside. pfrep_gap_realize_common_rightfirstoutside+(M)=(pfrep_power_realize_common_right)) /\ (((pfrep_left_realize_common_right)=0))))) -> ((exists pfrep_position_realize_common_rightsecond. ((pfrep_position_realize_common_rightsecond+S (pfrep_power_realize_common_right)=(K)) /\ ((((exists ff_h_pfp_realize_common_rightsecondentry. ff_h_pfp_realize_common_rightsecondentry + S (pfrep_right_realize_common_right) = S ((S (pfrep_position_realize_common_rightsecond)) * vc)) /\ exists ff_q_pfp_realize_common_rightsecondentry. vb = ff_q_pfp_realize_common_rightsecondentry * S ((S (pfrep_position_realize_common_rightsecond)) * vc) + (pfrep_right_realize_common_right)))))) \/ (((exists pfrep_gap_realize_common_rightsecondoutside. pfrep_gap_realize_common_rightsecondoutside+(K)=(pfrep_power_realize_common_right)) /\ (((pfrep_right_realize_common_right)=0))))) -> pfrep_left_realize_common_right=pfrep_right_realize_common_right)))) -> (forall pfrep_power_realize_output pfrep_left_realize_output pfrep_right_realize_output. ((exists pfrep_position_realize_outputfirst. ((pfrep_position_realize_outputfirst+S (pfrep_power_realize_output)=(N)) /\ ((((exists ff_h_pfp_realize_outputfirstentry. ff_h_pfp_realize_outputfirstentry + S (pfrep_left_realize_output) = S ((S (pfrep_position_realize_outputfirst)) * rc)) /\ exists ff_q_pfp_realize_outputfirstentry. rb = ff_q_pfp_realize_outputfirstentry * S ((S (pfrep_position_realize_outputfirst)) * rc) + (pfrep_left_realize_output)))))) \/ (((exists pfrep_gap_realize_outputfirstoutside. pfrep_gap_realize_outputfirstoutside+(N)=(pfrep_power_realize_output)) /\ (((pfrep_left_realize_output)=0))))) -> ((exists pfrep_position_realize_outputsecond. ((pfrep_position_realize_outputsecond+S (pfrep_power_realize_output)=(K)) /\ ((((exists ff_h_pfp_realize_outputsecondentry. ff_h_pfp_realize_outputsecondentry + S (pfrep_right_realize_output) = S ((S (pfrep_position_realize_outputsecond)) * tc)) /\ exists ff_q_pfp_realize_outputsecondentry. tb = ff_q_pfp_realize_outputsecondentry * S ((S (pfrep_position_realize_outputsecond)) * tc) + (pfrep_right_realize_output)))))) \/ (((exists pfrep_gap_realize_outputsecondoutside. pfrep_gap_realize_outputsecondoutside+(K)=(pfrep_power_realize_output)) /\ (((pfrep_right_realize_output)=0))))) -> pfrep_left_realize_output=pfrep_right_realize_output) -> (forall pfp_index_realize_actual_operation. (exists pfa_gap_realize_actual_operationindex. pfa_gap_realize_actual_operationindex + S (pfp_index_realize_actual_operation) = (K)) -> exists pfp_left_realize_actual_operation pfp_right_realize_actual_operation pfp_value_realize_actual_operation. ((((exists ff_h_pfp_realize_actual_operationleft. ff_h_pfp_realize_actual_operationleft + S (pfp_left_realize_actual_operation) = S ((S (pfp_index_realize_actual_operation)) * uc)) /\ exists ff_q_pfp_realize_actual_operationleft. ub = ff_q_pfp_realize_actual_operationleft * S ((S (pfp_index_realize_actual_operation)) * uc) + (pfp_left_realize_actual_operation))) /\ (((((exists ff_h_pfp_realize_actual_operationright. ff_h_pfp_realize_actual_operationright + S (pfp_right_realize_actual_operation) = S ((S (pfp_index_realize_actual_operation)) * vc)) /\ exists ff_q_pfp_realize_actual_operationright. vb = ff_q_pfp_realize_actual_operationright * S ((S (pfp_index_realize_actual_operation)) * vc) + (pfp_right_realize_actual_operation))) /\ (((((exists ff_h_pfp_realize_actual_operationtarget. ff_h_pfp_realize_actual_operationtarget + S (pfp_value_realize_actual_operation) = S ((S (pfp_index_realize_actual_operation)) * tc)) /\ exists ff_q_pfp_realize_actual_operationtarget. tb = ff_q_pfp_realize_actual_operationtarget * S ((S (pfp_index_realize_actual_operation)) * tc) + (pfp_value_realize_actual_operation))) /\ ((((exists pfa_gap_realize_actual_operationoperationleft. pfa_gap_realize_actual_operationoperationleft + S (pfp_left_realize_actual_operation) = (p)) /\ (((exists pfa_gap_realize_actual_operationoperationright. pfa_gap_realize_actual_operationoperationright + S (pfp_right_realize_actual_operation) = (p)) /\ ((((exists pfa_gap_realize_actual_operationoperationresultbound. pfa_gap_realize_actual_operationoperationresultbound + S (pfp_value_realize_actual_operation) = (p)) /\ ((exists pfa_offset_left_realize_actual_operationoperationresultcongruence pfa_offset_right_realize_actual_operationoperationresultcongruence. ((pfp_left_realize_actual_operation) + (pfp_right_realize_actual_operation)) + (p) * pfa_offset_left_realize_actual_operationoperationresultcongruence = (pfp_value_realize_actual_operation) + (p) * pfa_offset_right_realize_actual_operationoperationresultcongruence))))))))))))))))

Constructive proof overview

Generated structural guide

Realize the addition on any supplied canonical equal-length representatives: construct a sum, prove formal output uniqueness, then transport the actual operation by decoded coefficient equality.

The unchanged tactic script uses 8 declared prerequisites and contains 146 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_field_polynomial_add_exists Alpha theorem; checked-use authorized prime_nonzero Alpha theorem; checked-use authorized PG003E prime_field_polynomial_aligned_add_from_fixed PG003F prime_field_polynomial_aligned_add_transport prime_field_polynomial_equivalent_symmetric Alpha theorem; checked-use authorized PG0041 prime_field_polynomial_aligned_add_functional prime_field_polynomial_add_transport Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_implies_equal_same_length Alpha theorem; checked-use authorized

Direct dependents

PG0046 prime_field_polynomial_aligned_add_cancel_left PG0047 prime_field_polynomial_aligned_add_associative

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

146 script commands · 22 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 (3)
prime field polynomial aligned add from fixedprime field polynomial aligned add transportprime field polynomial aligned add 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–20

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

  1. L11
    intro ub
  2. L12
    intro uc
  3. L13
    intro vb
  4. L14
    intro vc
  5. L15
    intro tb
  6. L16
    intro tc
  7. L17
    intro K
  8. L18
    intro hp
  9. L19
    intro h
  10. L20
    intro hu
03Fix variables and assumptionsL21–24

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

  1. L21
    intro hv
  2. L22
    intro ht
  3. L23
    intro hc
  4. L24
    intro hr
04Separate the logical casesL25–25

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

  1. L25
    cases hc
05Establish hzL26–35

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

  1. L26
    have hz : ∃ zb. ∃ zc. FpPolyAdd(p,ub,uc,vb,vc,zb,zc,K)Definitions: FpPolyAdd
  2. L27
    specialize prime_field_polynomial_add_exists (p)
  3. L28
    specialize prime_field_polynomial_add_exists (ub)
  4. L29
    specialize prime_field_polynomial_add_exists (uc)
  5. L30
    specialize prime_field_polynomial_add_exists (vb)
  6. L31
    specialize prime_field_polynomial_add_exists (vc)
  7. L32
    specialize prime_field_polynomial_add_exists (K)
  8. L33
    apply prime_field_polynomial_add_exists
  9. L34
    intro hpzero
  10. L35
    specialize prime_nonzero (p)
06Use earlier factsL36–40

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

  1. L36
    apply prime_nonzero
  2. L37
    exact hp
  3. L38
    exact hpzero
  4. L39
    exact hu
  5. L40
    exact hv
07Separate the logical casesL41–42

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

  1. L41
    cases hz
  2. L42
    cases hz_witness
08Establish hzgraphL43–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial aligned add from fixed.

  1. L43
    have hzgraph : FpPolynomialAlignedAdd(p,ub,uc,K,vb,vc,K,x,x1,K)Definitions: FpPolynomialAlignedAdd
  2. L44
    specialize prime_field_polynomial_aligned_add_from_fixed (p)
  3. L45
    specialize prime_field_polynomial_aligned_add_from_fixed (ub)
  4. L46
    specialize prime_field_polynomial_aligned_add_from_fixed (uc)
  5. L47
    specialize prime_field_polynomial_aligned_add_from_fixed (vb)
  6. L48
    specialize prime_field_polynomial_aligned_add_from_fixed (vc)
  7. L49
    specialize prime_field_polynomial_aligned_add_from_fixed (x)
  8. L50
    specialize prime_field_polynomial_aligned_add_from_fixed (x1)
  9. L51
    specialize prime_field_polynomial_aligned_add_from_fixed (K)
  10. L52
    apply prime_field_polynomial_aligned_add_from_fixed
09Use earlier factsL53–53

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

  1. L53
    exact hz_witness_witness
10Establish htgraphL54–63

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

  1. L54
    have htgraph : FpPolynomialAlignedAdd(p,ub,uc,K,vb,vc,K,tb,tc,K)Definitions: FpPolynomialAlignedAdd
  2. L55
    specialize prime_field_polynomial_aligned_add_transport (p)
  3. L56
    specialize prime_field_polynomial_aligned_add_transport (ab)
  4. L57
    specialize prime_field_polynomial_aligned_add_transport (ac)
  5. L58
    specialize prime_field_polynomial_aligned_add_transport (L)
  6. L59
    specialize prime_field_polynomial_aligned_add_transport (bb)
  7. L60
    specialize prime_field_polynomial_aligned_add_transport (bc)
  8. L61
    specialize prime_field_polynomial_aligned_add_transport (M)
  9. L62
    specialize prime_field_polynomial_aligned_add_transport (rb)
  10. L63
    specialize prime_field_polynomial_aligned_add_transport (rc)
11Use earlier factsL64–73

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

  1. L64
    specialize prime_field_polynomial_aligned_add_transport (N)
  2. L65
    specialize prime_field_polynomial_aligned_add_transport (ub)
  3. L66
    specialize prime_field_polynomial_aligned_add_transport (uc)
  4. L67
    specialize prime_field_polynomial_aligned_add_transport (K)
  5. L68
    specialize prime_field_polynomial_aligned_add_transport (vb)
  6. L69
    specialize prime_field_polynomial_aligned_add_transport (vc)
  7. L70
    specialize prime_field_polynomial_aligned_add_transport (K)
  8. L71
    specialize prime_field_polynomial_aligned_add_transport (tb)
  9. L72
    specialize prime_field_polynomial_aligned_add_transport (tc)
  10. L73
    specialize prime_field_polynomial_aligned_add_transport (K)
12Use earlier factsL74–83

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

  1. L74
    apply prime_field_polynomial_aligned_add_transport
  2. L75
    exact hu
  3. L76
    exact hv
  4. L77
    exact ht
  5. L78
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  6. L79
    specialize prime_field_polynomial_equivalent_symmetric (ac)
  7. L80
    specialize prime_field_polynomial_equivalent_symmetric (L)
  8. L81
    specialize prime_field_polynomial_equivalent_symmetric (ub)
  9. L82
    specialize prime_field_polynomial_equivalent_symmetric (uc)
  10. L83
    specialize prime_field_polynomial_equivalent_symmetric (K)
13Use earlier factsL84–93

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

  1. L84
    apply prime_field_polynomial_equivalent_symmetric
  2. L85
    exact hc_left
  3. L86
    specialize prime_field_polynomial_equivalent_symmetric (bb)
  4. L87
    specialize prime_field_polynomial_equivalent_symmetric (bc)
  5. L88
    specialize prime_field_polynomial_equivalent_symmetric (M)
  6. L89
    specialize prime_field_polynomial_equivalent_symmetric (vb)
  7. L90
    specialize prime_field_polynomial_equivalent_symmetric (vc)
  8. L91
    specialize prime_field_polynomial_equivalent_symmetric (K)
  9. L92
    apply prime_field_polynomial_equivalent_symmetric
  10. L93
    exact hc_right
14Use earlier factsL94–95

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

  1. L94
    exact hr
  2. L95
    exact h
15Establish heL96–105

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

  1. L96
    have he : PolynomialEquivalent(x,x1,K,tb,tc,K)Definitions: PolynomialEquivalent
  2. L97
    specialize prime_field_polynomial_aligned_add_functional (p)
  3. L98
    specialize prime_field_polynomial_aligned_add_functional (ub)
  4. L99
    specialize prime_field_polynomial_aligned_add_functional (uc)
  5. L100
    specialize prime_field_polynomial_aligned_add_functional (K)
  6. L101
    specialize prime_field_polynomial_aligned_add_functional (vb)
  7. L102
    specialize prime_field_polynomial_aligned_add_functional (vc)
  8. L103
    specialize prime_field_polynomial_aligned_add_functional (K)
  9. L104
    specialize prime_field_polynomial_aligned_add_functional (x)
  10. L105
    specialize prime_field_polynomial_aligned_add_functional (x1)
16Use earlier factsL106–115

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

  1. L106
    specialize prime_field_polynomial_aligned_add_functional (K)
  2. L107
    specialize prime_field_polynomial_aligned_add_functional (tb)
  3. L108
    specialize prime_field_polynomial_aligned_add_functional (tc)
  4. L109
    specialize prime_field_polynomial_aligned_add_functional (K)
  5. L110
    apply prime_field_polynomial_aligned_add_functional
  6. L111
    exact hp
  7. L112
    exact hzgraph
  8. L113
    exact htgraph
  9. L114
    specialize prime_field_polynomial_add_transport (p)
  10. L115
    specialize prime_field_polynomial_add_transport (ub)
17Use earlier factsL116–125

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

  1. L116
    specialize prime_field_polynomial_add_transport (uc)
  2. L117
    specialize prime_field_polynomial_add_transport (vb)
  3. L118
    specialize prime_field_polynomial_add_transport (vc)
  4. L119
    specialize prime_field_polynomial_add_transport (x)
  5. L120
    specialize prime_field_polynomial_add_transport (x1)
  6. L121
    specialize prime_field_polynomial_add_transport (ub)
  7. L122
    specialize prime_field_polynomial_add_transport (uc)
  8. L123
    specialize prime_field_polynomial_add_transport (vb)
  9. L124
    specialize prime_field_polynomial_add_transport (vc)
  10. L125
    specialize prime_field_polynomial_add_transport (tb)
18Use earlier factsL126–128

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

  1. L126
    specialize prime_field_polynomial_add_transport (tc)
  2. L127
    specialize prime_field_polynomial_add_transport (K)
  3. L128
    apply prime_field_polynomial_add_transport
19Fix variables and assumptionsL129–132

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

  1. L129
    intro i
  2. L130
    intro a
  3. L131
    intro hi
  4. L132
    intro ha
20Use earlier factsL133–133

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

  1. L133
    exact ha
21Fix variables and assumptionsL134–137

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

  1. L134
    intro i
  2. L135
    intro a
  3. L136
    intro hi
  4. L137
    intro ha
22Use earlier factsL138–146

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

  1. L138
    exact ha
  2. L139
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (x)
  3. L140
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (x1)
  4. L141
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (tb)
  5. L142
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (tc)
  6. L143
    specialize prime_field_polynomial_equivalent_implies_equal_same_length (K)
  7. L144
    apply prime_field_polynomial_equivalent_implies_equal_same_length
  8. L145
    exact he
  9. L146
    exact hz_witness_witness

Library-wide reading audit

Original exact command ledger · 146 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 ub
  12. 0012intro uc
  13. 0013intro vb
  14. 0014intro vc
  15. 0015intro tb
  16. 0016intro tc
  17. 0017intro K
  18. 0018intro hp
  19. 0019intro h
  20. 0020intro hu
  21. 0021intro hv
  22. 0022intro ht
  23. 0023intro hc
  24. 0024intro hr
  25. 0025cases hc
  26. 0026have hz : exists zb zc. forall pfp_index_realize_constructed_sum. (exists pfa_gap_realize_constructed_sumindex. pfa_gap_realize_constructed_sumindex + S (pfp_index_realize_constructed_sum) = (K)) -> exists pfp_left_realize_constructed_sum pfp_right_realize_constructed_sum pfp_value_realize_constructed_sum. ((((exists ff_h_pfp_realize_constructed_sumleft. ff_h_pfp_realize_constructed_sumleft + S (pfp_left_realize_constructed_sum) = S ((S (pfp_index_realize_constructed_sum)) * uc)) /\ exists ff_q_pfp_realize_constructed_sumleft. ub = ff_q_pfp_realize_constructed_sumleft * S ((S (pfp_index_realize_constructed_sum)) * uc) + (pfp_left_realize_constructed_sum))) /\ (((((exists ff_h_pfp_realize_constructed_sumright. ff_h_pfp_realize_constructed_sumright + S (pfp_right_realize_constructed_sum) = S ((S (pfp_index_realize_constructed_sum)) * vc)) /\ exists ff_q_pfp_realize_constructed_sumright. vb = ff_q_pfp_realize_constructed_sumright * S ((S (pfp_index_realize_constructed_sum)) * vc) + (pfp_right_realize_constructed_sum))) /\ (((((exists ff_h_pfp_realize_constructed_sumtarget. ff_h_pfp_realize_constructed_sumtarget + S (pfp_value_realize_constructed_sum) = S ((S (pfp_index_realize_constructed_sum)) * zc)) /\ exists ff_q_pfp_realize_constructed_sumtarget. zb = ff_q_pfp_realize_constructed_sumtarget * S ((S (pfp_index_realize_constructed_sum)) * zc) + (pfp_value_realize_constructed_sum))) /\ ((((exists pfa_gap_realize_constructed_sumoperationleft. pfa_gap_realize_constructed_sumoperationleft + S (pfp_left_realize_constructed_sum) = (p)) /\ (((exists pfa_gap_realize_constructed_sumoperationright. pfa_gap_realize_constructed_sumoperationright + S (pfp_right_realize_constructed_sum) = (p)) /\ ((((exists pfa_gap_realize_constructed_sumoperationresultbound. pfa_gap_realize_constructed_sumoperationresultbound + S (pfp_value_realize_constructed_sum) = (p)) /\ ((exists pfa_offset_left_realize_constructed_sumoperationresultcongruence pfa_offset_right_realize_constructed_sumoperationresultcongruence. ((pfp_left_realize_constructed_sum) + (pfp_right_realize_constructed_sum)) + (p) * pfa_offset_left_realize_constructed_sumoperationresultcongruence = (pfp_value_realize_constructed_sum) + (p) * pfa_offset_right_realize_constructed_sumoperationresultcongruence)))))))))))))))
  27. 0027specialize prime_field_polynomial_add_exists (p)
  28. 0028specialize prime_field_polynomial_add_exists (ub)
  29. 0029specialize prime_field_polynomial_add_exists (uc)
  30. 0030specialize prime_field_polynomial_add_exists (vb)
  31. 0031specialize prime_field_polynomial_add_exists (vc)
  32. 0032specialize prime_field_polynomial_add_exists (K)
  33. 0033apply prime_field_polynomial_add_exists
  34. 0034intro hpzero
  35. 0035specialize prime_nonzero (p)
  36. 0036apply prime_nonzero
  37. 0037exact hp
  38. 0038exact hpzero
  39. 0039exact hu
  40. 0040exact hv
  41. 0041cases hz
  42. 0042cases hz_witness
  43. 0043have hzgraph : ((forall fom_index_pfp_realize_constructed_graph_left_bounded. (exists fom_gap_pfp_realize_constructed_graph_left_bounded_index_bound. fom_gap_pfp_realize_constructed_graph_left_bounded_index_bound + S (fom_index_pfp_realize_constructed_graph_left_bounded) = K) -> exists fom_value_pfp_realize_constructed_graph_left_bounded. ((((exists fom_beta_height_pfp_realize_constructed_graph_left_bounded_entry. fom_beta_height_pfp_realize_constructed_graph_left_bounded_entry + S (fom_value_pfp_realize_constructed_graph_left_bounded) = S ((S (fom_index_pfp_realize_constructed_graph_left_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_realize_constructed_graph_left_bounded_entry. ub = fom_beta_quotient_pfp_realize_constructed_graph_left_bounded_entry * S ((S (fom_index_pfp_realize_constructed_graph_left_bounded)) * uc) + (fom_value_pfp_realize_constructed_graph_left_bounded))) /\ (exists fom_gap_pfp_realize_constructed_graph_left_bounded_value_bound. fom_gap_pfp_realize_constructed_graph_left_bounded_value_bound + S (fom_value_pfp_realize_constructed_graph_left_bounded) = p))) /\ (((forall fom_index_pfp_realize_constructed_graph_right_bounded. (exists fom_gap_pfp_realize_constructed_graph_right_bounded_index_bound. fom_gap_pfp_realize_constructed_graph_right_bounded_index_bound + S (fom_index_pfp_realize_constructed_graph_right_bounded) = K) -> exists fom_value_pfp_realize_constructed_graph_right_bounded. ((((exists fom_beta_height_pfp_realize_constructed_graph_right_bounded_entry. fom_beta_height_pfp_realize_constructed_graph_right_bounded_entry + S (fom_value_pfp_realize_constructed_graph_right_bounded) = S ((S (fom_index_pfp_realize_constructed_graph_right_bounded)) * vc)) /\ exists fom_beta_quotient_pfp_realize_constructed_graph_right_bounded_entry. vb = fom_beta_quotient_pfp_realize_constructed_graph_right_bounded_entry * S ((S (fom_index_pfp_realize_constructed_graph_right_bounded)) * vc) + (fom_value_pfp_realize_constructed_graph_right_bounded))) /\ (exists fom_gap_pfp_realize_constructed_graph_right_bounded_value_bound. fom_gap_pfp_realize_constructed_graph_right_bounded_value_bound + S (fom_value_pfp_realize_constructed_graph_right_bounded) = p))) /\ (((forall fom_index_pfp_realize_constructed_graph_result_bounded. (exists fom_gap_pfp_realize_constructed_graph_result_bounded_index_bound. fom_gap_pfp_realize_constructed_graph_result_bounded_index_bound + S (fom_index_pfp_realize_constructed_graph_result_bounded) = K) -> exists fom_value_pfp_realize_constructed_graph_result_bounded. ((((exists fom_beta_height_pfp_realize_constructed_graph_result_bounded_entry. fom_beta_height_pfp_realize_constructed_graph_result_bounded_entry + S (fom_value_pfp_realize_constructed_graph_result_bounded) = S ((S (fom_index_pfp_realize_constructed_graph_result_bounded)) * x1)) /\ exists fom_beta_quotient_pfp_realize_constructed_graph_result_bounded_entry. x = fom_beta_quotient_pfp_realize_constructed_graph_result_bounded_entry * S ((S (fom_index_pfp_realize_constructed_graph_result_bounded)) * x1) + (fom_value_pfp_realize_constructed_graph_result_bounded))) /\ (exists fom_gap_pfp_realize_constructed_graph_result_bounded_value_bound. fom_gap_pfp_realize_constructed_graph_result_bounded_value_bound + S (fom_value_pfp_realize_constructed_graph_result_bounded) = p))) /\ ((exists pfaa_left_b_realize_constructed_graph pfaa_left_c_realize_constructed_graph pfaa_right_b_realize_constructed_graph pfaa_right_c_realize_constructed_graph pfaa_sum_b_realize_constructed_graph pfaa_sum_c_realize_constructed_graph pfaa_length_realize_constructed_graph. ((((forall pfrep_power_realize_constructed_graph_witness_common_left pfrep_left_realize_constructed_graph_witness_common_left pfrep_right_realize_constructed_graph_witness_common_left. ((exists pfrep_position_realize_constructed_graph_witness_common_leftfirst. ((pfrep_position_realize_constructed_graph_witness_common_leftfirst+S (pfrep_power_realize_constructed_graph_witness_common_left)=(K)) /\ ((((exists ff_h_pfp_realize_constructed_graph_witness_common_leftfirstentry. ff_h_pfp_realize_constructed_graph_witness_common_leftfirstentry + S (pfrep_left_realize_constructed_graph_witness_common_left) = S ((S (pfrep_position_realize_constructed_graph_witness_common_leftfirst)) * uc)) /\ exists ff_q_pfp_realize_constructed_graph_witness_common_leftfirstentry. ub = ff_q_pfp_realize_constructed_graph_witness_common_leftfirstentry * S ((S (pfrep_position_realize_constructed_graph_witness_common_leftfirst)) * uc) + (pfrep_left_realize_constructed_graph_witness_common_left)))))) \/ (((exists pfrep_gap_realize_constructed_graph_witness_common_leftfirstoutside. pfrep_gap_realize_constructed_graph_witness_common_leftfirstoutside+(K)=(pfrep_power_realize_constructed_graph_witness_common_left)) /\ (((pfrep_left_realize_constructed_graph_witness_common_left)=0))))) -> ((exists pfrep_position_realize_constructed_graph_witness_common_leftsecond. ((pfrep_position_realize_constructed_graph_witness_common_leftsecond+S (pfrep_power_realize_constructed_graph_witness_common_left)=(pfaa_length_realize_constructed_graph)) /\ ((((exists ff_h_pfp_realize_constructed_graph_witness_common_leftsecondentry. ff_h_pfp_realize_constructed_graph_witness_common_leftsecondentry + S (pfrep_right_realize_constructed_graph_witness_common_left) = S ((S (pfrep_position_realize_constructed_graph_witness_common_leftsecond)) * pfaa_left_c_realize_constructed_graph)) /\ exists ff_q_pfp_realize_constructed_graph_witness_common_leftsecondentry. pfaa_left_b_realize_constructed_graph = ff_q_pfp_realize_constructed_graph_witness_common_leftsecondentry * S ((S (pfrep_position_realize_constructed_graph_witness_common_leftsecond)) * pfaa_left_c_realize_constructed_graph) + (pfrep_right_realize_constructed_graph_witness_common_left)))))) \/ (((exists pfrep_gap_realize_constructed_graph_witness_common_leftsecondoutside. pfrep_gap_realize_constructed_graph_witness_common_leftsecondoutside+(pfaa_length_realize_constructed_graph)=(pfrep_power_realize_constructed_graph_witness_common_left)) /\ (((pfrep_right_realize_constructed_graph_witness_common_left)=0))))) -> pfrep_left_realize_constructed_graph_witness_common_left=pfrep_right_realize_constructed_graph_witness_common_left) /\ ((forall pfrep_power_realize_constructed_graph_witness_common_right pfrep_left_realize_constructed_graph_witness_common_right pfrep_right_realize_constructed_graph_witness_common_right. ((exists pfrep_position_realize_constructed_graph_witness_common_rightfirst. ((pfrep_position_realize_constructed_graph_witness_common_rightfirst+S (pfrep_power_realize_constructed_graph_witness_common_right)=(K)) /\ ((((exists ff_h_pfp_realize_constructed_graph_witness_common_rightfirstentry. ff_h_pfp_realize_constructed_graph_witness_common_rightfirstentry + S (pfrep_left_realize_constructed_graph_witness_common_right) = S ((S (pfrep_position_realize_constructed_graph_witness_common_rightfirst)) * vc)) /\ exists ff_q_pfp_realize_constructed_graph_witness_common_rightfirstentry. vb = ff_q_pfp_realize_constructed_graph_witness_common_rightfirstentry * S ((S (pfrep_position_realize_constructed_graph_witness_common_rightfirst)) * vc) + (pfrep_left_realize_constructed_graph_witness_common_right)))))) \/ (((exists pfrep_gap_realize_constructed_graph_witness_common_rightfirstoutside. pfrep_gap_realize_constructed_graph_witness_common_rightfirstoutside+(K)=(pfrep_power_realize_constructed_graph_witness_common_right)) /\ (((pfrep_left_realize_constructed_graph_witness_common_right)=0))))) -> ((exists pfrep_position_realize_constructed_graph_witness_common_rightsecond. ((pfrep_position_realize_constructed_graph_witness_common_rightsecond+S (pfrep_power_realize_constructed_graph_witness_common_right)=(pfaa_length_realize_constructed_graph)) /\ ((((exists ff_h_pfp_realize_constructed_graph_witness_common_rightsecondentry. ff_h_pfp_realize_constructed_graph_witness_common_rightsecondentry + S (pfrep_right_realize_constructed_graph_witness_common_right) = S ((S (pfrep_position_realize_constructed_graph_witness_common_rightsecond)) * pfaa_right_c_realize_constructed_graph)) /\ exists ff_q_pfp_realize_constructed_graph_witness_common_rightsecondentry. pfaa_right_b_realize_constructed_graph = ff_q_pfp_realize_constructed_graph_witness_common_rightsecondentry * S ((S (pfrep_position_realize_constructed_graph_witness_common_rightsecond)) * pfaa_right_c_realize_constructed_graph) + (pfrep_right_realize_constructed_graph_witness_common_right)))))) \/ (((exists pfrep_gap_realize_constructed_graph_witness_common_rightsecondoutside. pfrep_gap_realize_constructed_graph_witness_common_rightsecondoutside+(pfaa_length_realize_constructed_graph)=(pfrep_power_realize_constructed_graph_witness_common_right)) /\ (((pfrep_right_realize_constructed_graph_witness_common_right)=0))))) -> pfrep_left_realize_constructed_graph_witness_common_right=pfrep_right_realize_constructed_graph_witness_common_right)))) /\ (((forall pfp_index_realize_constructed_graph_witness_operation. (exists pfa_gap_realize_constructed_graph_witness_operationindex. pfa_gap_realize_constructed_graph_witness_operationindex + S (pfp_index_realize_constructed_graph_witness_operation) = (pfaa_length_realize_constructed_graph)) -> exists pfp_left_realize_constructed_graph_witness_operation pfp_right_realize_constructed_graph_witness_operation pfp_value_realize_constructed_graph_witness_operation. ((((exists ff_h_pfp_realize_constructed_graph_witness_operationleft. ff_h_pfp_realize_constructed_graph_witness_operationleft + S (pfp_left_realize_constructed_graph_witness_operation) = S ((S (pfp_index_realize_constructed_graph_witness_operation)) * pfaa_left_c_realize_constructed_graph)) /\ exists ff_q_pfp_realize_constructed_graph_witness_operationleft. pfaa_left_b_realize_constructed_graph = ff_q_pfp_realize_constructed_graph_witness_operationleft * S ((S (pfp_index_realize_constructed_graph_witness_operation)) * pfaa_left_c_realize_constructed_graph) + (pfp_left_realize_constructed_graph_witness_operation))) /\ (((((exists ff_h_pfp_realize_constructed_graph_witness_operationright. ff_h_pfp_realize_constructed_graph_witness_operationright + S (pfp_right_realize_constructed_graph_witness_operation) = S ((S (pfp_index_realize_constructed_graph_witness_operation)) * pfaa_right_c_realize_constructed_graph)) /\ exists ff_q_pfp_realize_constructed_graph_witness_operationright. pfaa_right_b_realize_constructed_graph = ff_q_pfp_realize_constructed_graph_witness_operationright * S ((S (pfp_index_realize_constructed_graph_witness_operation)) * pfaa_right_c_realize_constructed_graph) + (pfp_right_realize_constructed_graph_witness_operation))) /\ (((((exists ff_h_pfp_realize_constructed_graph_witness_operationtarget. ff_h_pfp_realize_constructed_graph_witness_operationtarget + S (pfp_value_realize_constructed_graph_witness_operation) = S ((S (pfp_index_realize_constructed_graph_witness_operation)) * pfaa_sum_c_realize_constructed_graph)) /\ exists ff_q_pfp_realize_constructed_graph_witness_operationtarget. pfaa_sum_b_realize_constructed_graph = ff_q_pfp_realize_constructed_graph_witness_operationtarget * S ((S (pfp_index_realize_constructed_graph_witness_operation)) * pfaa_sum_c_realize_constructed_graph) + (pfp_value_realize_constructed_graph_witness_operation))) /\ ((((exists pfa_gap_realize_constructed_graph_witness_operationoperationleft. pfa_gap_realize_constructed_graph_witness_operationoperationleft + S (pfp_left_realize_constructed_graph_witness_operation) = (p)) /\ (((exists pfa_gap_realize_constructed_graph_witness_operationoperationright. pfa_gap_realize_constructed_graph_witness_operationoperationright + S (pfp_right_realize_constructed_graph_witness_operation) = (p)) /\ ((((exists pfa_gap_realize_constructed_graph_witness_operationoperationresultbound. pfa_gap_realize_constructed_graph_witness_operationoperationresultbound + S (pfp_value_realize_constructed_graph_witness_operation) = (p)) /\ ((exists pfa_offset_left_realize_constructed_graph_witness_operationoperationresultcongruence pfa_offset_right_realize_constructed_graph_witness_operationoperationresultcongruence. ((pfp_left_realize_constructed_graph_witness_operation) + (pfp_right_realize_constructed_graph_witness_operation)) + (p) * pfa_offset_left_realize_constructed_graph_witness_operationoperationresultcongruence = (pfp_value_realize_constructed_graph_witness_operation) + (p) * pfa_offset_right_realize_constructed_graph_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_realize_constructed_graph_witness_output pfrep_left_realize_constructed_graph_witness_output pfrep_right_realize_constructed_graph_witness_output. ((exists pfrep_position_realize_constructed_graph_witness_outputfirst. ((pfrep_position_realize_constructed_graph_witness_outputfirst+S (pfrep_power_realize_constructed_graph_witness_output)=(pfaa_length_realize_constructed_graph)) /\ ((((exists ff_h_pfp_realize_constructed_graph_witness_outputfirstentry. ff_h_pfp_realize_constructed_graph_witness_outputfirstentry + S (pfrep_left_realize_constructed_graph_witness_output) = S ((S (pfrep_position_realize_constructed_graph_witness_outputfirst)) * pfaa_sum_c_realize_constructed_graph)) /\ exists ff_q_pfp_realize_constructed_graph_witness_outputfirstentry. pfaa_sum_b_realize_constructed_graph = ff_q_pfp_realize_constructed_graph_witness_outputfirstentry * S ((S (pfrep_position_realize_constructed_graph_witness_outputfirst)) * pfaa_sum_c_realize_constructed_graph) + (pfrep_left_realize_constructed_graph_witness_output)))))) \/ (((exists pfrep_gap_realize_constructed_graph_witness_outputfirstoutside. pfrep_gap_realize_constructed_graph_witness_outputfirstoutside+(pfaa_length_realize_constructed_graph)=(pfrep_power_realize_constructed_graph_witness_output)) /\ (((pfrep_left_realize_constructed_graph_witness_output)=0))))) -> ((exists pfrep_position_realize_constructed_graph_witness_outputsecond. ((pfrep_position_realize_constructed_graph_witness_outputsecond+S (pfrep_power_realize_constructed_graph_witness_output)=(K)) /\ ((((exists ff_h_pfp_realize_constructed_graph_witness_outputsecondentry. ff_h_pfp_realize_constructed_graph_witness_outputsecondentry + S (pfrep_right_realize_constructed_graph_witness_output) = S ((S (pfrep_position_realize_constructed_graph_witness_outputsecond)) * x1)) /\ exists ff_q_pfp_realize_constructed_graph_witness_outputsecondentry. x = ff_q_pfp_realize_constructed_graph_witness_outputsecondentry * S ((S (pfrep_position_realize_constructed_graph_witness_outputsecond)) * x1) + (pfrep_right_realize_constructed_graph_witness_output)))))) \/ (((exists pfrep_gap_realize_constructed_graph_witness_outputsecondoutside. pfrep_gap_realize_constructed_graph_witness_outputsecondoutside+(K)=(pfrep_power_realize_constructed_graph_witness_output)) /\ (((pfrep_right_realize_constructed_graph_witness_output)=0))))) -> pfrep_left_realize_constructed_graph_witness_output=pfrep_right_realize_constructed_graph_witness_output))))))))))))
  44. 0044specialize prime_field_polynomial_aligned_add_from_fixed (p)
  45. 0045specialize prime_field_polynomial_aligned_add_from_fixed (ub)
  46. 0046specialize prime_field_polynomial_aligned_add_from_fixed (uc)
  47. 0047specialize prime_field_polynomial_aligned_add_from_fixed (vb)
  48. 0048specialize prime_field_polynomial_aligned_add_from_fixed (vc)
  49. 0049specialize prime_field_polynomial_aligned_add_from_fixed (x)
  50. 0050specialize prime_field_polynomial_aligned_add_from_fixed (x1)
  51. 0051specialize prime_field_polynomial_aligned_add_from_fixed (K)
  52. 0052apply prime_field_polynomial_aligned_add_from_fixed
  53. 0053exact hz_witness_witness
  54. 0054have htgraph : ((forall fom_index_pfp_realize_target_graph_left_bounded. (exists fom_gap_pfp_realize_target_graph_left_bounded_index_bound. fom_gap_pfp_realize_target_graph_left_bounded_index_bound + S (fom_index_pfp_realize_target_graph_left_bounded) = K) -> exists fom_value_pfp_realize_target_graph_left_bounded. ((((exists fom_beta_height_pfp_realize_target_graph_left_bounded_entry. fom_beta_height_pfp_realize_target_graph_left_bounded_entry + S (fom_value_pfp_realize_target_graph_left_bounded) = S ((S (fom_index_pfp_realize_target_graph_left_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_realize_target_graph_left_bounded_entry. ub = fom_beta_quotient_pfp_realize_target_graph_left_bounded_entry * S ((S (fom_index_pfp_realize_target_graph_left_bounded)) * uc) + (fom_value_pfp_realize_target_graph_left_bounded))) /\ (exists fom_gap_pfp_realize_target_graph_left_bounded_value_bound. fom_gap_pfp_realize_target_graph_left_bounded_value_bound + S (fom_value_pfp_realize_target_graph_left_bounded) = p))) /\ (((forall fom_index_pfp_realize_target_graph_right_bounded. (exists fom_gap_pfp_realize_target_graph_right_bounded_index_bound. fom_gap_pfp_realize_target_graph_right_bounded_index_bound + S (fom_index_pfp_realize_target_graph_right_bounded) = K) -> exists fom_value_pfp_realize_target_graph_right_bounded. ((((exists fom_beta_height_pfp_realize_target_graph_right_bounded_entry. fom_beta_height_pfp_realize_target_graph_right_bounded_entry + S (fom_value_pfp_realize_target_graph_right_bounded) = S ((S (fom_index_pfp_realize_target_graph_right_bounded)) * vc)) /\ exists fom_beta_quotient_pfp_realize_target_graph_right_bounded_entry. vb = fom_beta_quotient_pfp_realize_target_graph_right_bounded_entry * S ((S (fom_index_pfp_realize_target_graph_right_bounded)) * vc) + (fom_value_pfp_realize_target_graph_right_bounded))) /\ (exists fom_gap_pfp_realize_target_graph_right_bounded_value_bound. fom_gap_pfp_realize_target_graph_right_bounded_value_bound + S (fom_value_pfp_realize_target_graph_right_bounded) = p))) /\ (((forall fom_index_pfp_realize_target_graph_result_bounded. (exists fom_gap_pfp_realize_target_graph_result_bounded_index_bound. fom_gap_pfp_realize_target_graph_result_bounded_index_bound + S (fom_index_pfp_realize_target_graph_result_bounded) = K) -> exists fom_value_pfp_realize_target_graph_result_bounded. ((((exists fom_beta_height_pfp_realize_target_graph_result_bounded_entry. fom_beta_height_pfp_realize_target_graph_result_bounded_entry + S (fom_value_pfp_realize_target_graph_result_bounded) = S ((S (fom_index_pfp_realize_target_graph_result_bounded)) * tc)) /\ exists fom_beta_quotient_pfp_realize_target_graph_result_bounded_entry. tb = fom_beta_quotient_pfp_realize_target_graph_result_bounded_entry * S ((S (fom_index_pfp_realize_target_graph_result_bounded)) * tc) + (fom_value_pfp_realize_target_graph_result_bounded))) /\ (exists fom_gap_pfp_realize_target_graph_result_bounded_value_bound. fom_gap_pfp_realize_target_graph_result_bounded_value_bound + S (fom_value_pfp_realize_target_graph_result_bounded) = p))) /\ ((exists pfaa_left_b_realize_target_graph pfaa_left_c_realize_target_graph pfaa_right_b_realize_target_graph pfaa_right_c_realize_target_graph pfaa_sum_b_realize_target_graph pfaa_sum_c_realize_target_graph pfaa_length_realize_target_graph. ((((forall pfrep_power_realize_target_graph_witness_common_left pfrep_left_realize_target_graph_witness_common_left pfrep_right_realize_target_graph_witness_common_left. ((exists pfrep_position_realize_target_graph_witness_common_leftfirst. ((pfrep_position_realize_target_graph_witness_common_leftfirst+S (pfrep_power_realize_target_graph_witness_common_left)=(K)) /\ ((((exists ff_h_pfp_realize_target_graph_witness_common_leftfirstentry. ff_h_pfp_realize_target_graph_witness_common_leftfirstentry + S (pfrep_left_realize_target_graph_witness_common_left) = S ((S (pfrep_position_realize_target_graph_witness_common_leftfirst)) * uc)) /\ exists ff_q_pfp_realize_target_graph_witness_common_leftfirstentry. ub = ff_q_pfp_realize_target_graph_witness_common_leftfirstentry * S ((S (pfrep_position_realize_target_graph_witness_common_leftfirst)) * uc) + (pfrep_left_realize_target_graph_witness_common_left)))))) \/ (((exists pfrep_gap_realize_target_graph_witness_common_leftfirstoutside. pfrep_gap_realize_target_graph_witness_common_leftfirstoutside+(K)=(pfrep_power_realize_target_graph_witness_common_left)) /\ (((pfrep_left_realize_target_graph_witness_common_left)=0))))) -> ((exists pfrep_position_realize_target_graph_witness_common_leftsecond. ((pfrep_position_realize_target_graph_witness_common_leftsecond+S (pfrep_power_realize_target_graph_witness_common_left)=(pfaa_length_realize_target_graph)) /\ ((((exists ff_h_pfp_realize_target_graph_witness_common_leftsecondentry. ff_h_pfp_realize_target_graph_witness_common_leftsecondentry + S (pfrep_right_realize_target_graph_witness_common_left) = S ((S (pfrep_position_realize_target_graph_witness_common_leftsecond)) * pfaa_left_c_realize_target_graph)) /\ exists ff_q_pfp_realize_target_graph_witness_common_leftsecondentry. pfaa_left_b_realize_target_graph = ff_q_pfp_realize_target_graph_witness_common_leftsecondentry * S ((S (pfrep_position_realize_target_graph_witness_common_leftsecond)) * pfaa_left_c_realize_target_graph) + (pfrep_right_realize_target_graph_witness_common_left)))))) \/ (((exists pfrep_gap_realize_target_graph_witness_common_leftsecondoutside. pfrep_gap_realize_target_graph_witness_common_leftsecondoutside+(pfaa_length_realize_target_graph)=(pfrep_power_realize_target_graph_witness_common_left)) /\ (((pfrep_right_realize_target_graph_witness_common_left)=0))))) -> pfrep_left_realize_target_graph_witness_common_left=pfrep_right_realize_target_graph_witness_common_left) /\ ((forall pfrep_power_realize_target_graph_witness_common_right pfrep_left_realize_target_graph_witness_common_right pfrep_right_realize_target_graph_witness_common_right. ((exists pfrep_position_realize_target_graph_witness_common_rightfirst. ((pfrep_position_realize_target_graph_witness_common_rightfirst+S (pfrep_power_realize_target_graph_witness_common_right)=(K)) /\ ((((exists ff_h_pfp_realize_target_graph_witness_common_rightfirstentry. ff_h_pfp_realize_target_graph_witness_common_rightfirstentry + S (pfrep_left_realize_target_graph_witness_common_right) = S ((S (pfrep_position_realize_target_graph_witness_common_rightfirst)) * vc)) /\ exists ff_q_pfp_realize_target_graph_witness_common_rightfirstentry. vb = ff_q_pfp_realize_target_graph_witness_common_rightfirstentry * S ((S (pfrep_position_realize_target_graph_witness_common_rightfirst)) * vc) + (pfrep_left_realize_target_graph_witness_common_right)))))) \/ (((exists pfrep_gap_realize_target_graph_witness_common_rightfirstoutside. pfrep_gap_realize_target_graph_witness_common_rightfirstoutside+(K)=(pfrep_power_realize_target_graph_witness_common_right)) /\ (((pfrep_left_realize_target_graph_witness_common_right)=0))))) -> ((exists pfrep_position_realize_target_graph_witness_common_rightsecond. ((pfrep_position_realize_target_graph_witness_common_rightsecond+S (pfrep_power_realize_target_graph_witness_common_right)=(pfaa_length_realize_target_graph)) /\ ((((exists ff_h_pfp_realize_target_graph_witness_common_rightsecondentry. ff_h_pfp_realize_target_graph_witness_common_rightsecondentry + S (pfrep_right_realize_target_graph_witness_common_right) = S ((S (pfrep_position_realize_target_graph_witness_common_rightsecond)) * pfaa_right_c_realize_target_graph)) /\ exists ff_q_pfp_realize_target_graph_witness_common_rightsecondentry. pfaa_right_b_realize_target_graph = ff_q_pfp_realize_target_graph_witness_common_rightsecondentry * S ((S (pfrep_position_realize_target_graph_witness_common_rightsecond)) * pfaa_right_c_realize_target_graph) + (pfrep_right_realize_target_graph_witness_common_right)))))) \/ (((exists pfrep_gap_realize_target_graph_witness_common_rightsecondoutside. pfrep_gap_realize_target_graph_witness_common_rightsecondoutside+(pfaa_length_realize_target_graph)=(pfrep_power_realize_target_graph_witness_common_right)) /\ (((pfrep_right_realize_target_graph_witness_common_right)=0))))) -> pfrep_left_realize_target_graph_witness_common_right=pfrep_right_realize_target_graph_witness_common_right)))) /\ (((forall pfp_index_realize_target_graph_witness_operation. (exists pfa_gap_realize_target_graph_witness_operationindex. pfa_gap_realize_target_graph_witness_operationindex + S (pfp_index_realize_target_graph_witness_operation) = (pfaa_length_realize_target_graph)) -> exists pfp_left_realize_target_graph_witness_operation pfp_right_realize_target_graph_witness_operation pfp_value_realize_target_graph_witness_operation. ((((exists ff_h_pfp_realize_target_graph_witness_operationleft. ff_h_pfp_realize_target_graph_witness_operationleft + S (pfp_left_realize_target_graph_witness_operation) = S ((S (pfp_index_realize_target_graph_witness_operation)) * pfaa_left_c_realize_target_graph)) /\ exists ff_q_pfp_realize_target_graph_witness_operationleft. pfaa_left_b_realize_target_graph = ff_q_pfp_realize_target_graph_witness_operationleft * S ((S (pfp_index_realize_target_graph_witness_operation)) * pfaa_left_c_realize_target_graph) + (pfp_left_realize_target_graph_witness_operation))) /\ (((((exists ff_h_pfp_realize_target_graph_witness_operationright. ff_h_pfp_realize_target_graph_witness_operationright + S (pfp_right_realize_target_graph_witness_operation) = S ((S (pfp_index_realize_target_graph_witness_operation)) * pfaa_right_c_realize_target_graph)) /\ exists ff_q_pfp_realize_target_graph_witness_operationright. pfaa_right_b_realize_target_graph = ff_q_pfp_realize_target_graph_witness_operationright * S ((S (pfp_index_realize_target_graph_witness_operation)) * pfaa_right_c_realize_target_graph) + (pfp_right_realize_target_graph_witness_operation))) /\ (((((exists ff_h_pfp_realize_target_graph_witness_operationtarget. ff_h_pfp_realize_target_graph_witness_operationtarget + S (pfp_value_realize_target_graph_witness_operation) = S ((S (pfp_index_realize_target_graph_witness_operation)) * pfaa_sum_c_realize_target_graph)) /\ exists ff_q_pfp_realize_target_graph_witness_operationtarget. pfaa_sum_b_realize_target_graph = ff_q_pfp_realize_target_graph_witness_operationtarget * S ((S (pfp_index_realize_target_graph_witness_operation)) * pfaa_sum_c_realize_target_graph) + (pfp_value_realize_target_graph_witness_operation))) /\ ((((exists pfa_gap_realize_target_graph_witness_operationoperationleft. pfa_gap_realize_target_graph_witness_operationoperationleft + S (pfp_left_realize_target_graph_witness_operation) = (p)) /\ (((exists pfa_gap_realize_target_graph_witness_operationoperationright. pfa_gap_realize_target_graph_witness_operationoperationright + S (pfp_right_realize_target_graph_witness_operation) = (p)) /\ ((((exists pfa_gap_realize_target_graph_witness_operationoperationresultbound. pfa_gap_realize_target_graph_witness_operationoperationresultbound + S (pfp_value_realize_target_graph_witness_operation) = (p)) /\ ((exists pfa_offset_left_realize_target_graph_witness_operationoperationresultcongruence pfa_offset_right_realize_target_graph_witness_operationoperationresultcongruence. ((pfp_left_realize_target_graph_witness_operation) + (pfp_right_realize_target_graph_witness_operation)) + (p) * pfa_offset_left_realize_target_graph_witness_operationoperationresultcongruence = (pfp_value_realize_target_graph_witness_operation) + (p) * pfa_offset_right_realize_target_graph_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_realize_target_graph_witness_output pfrep_left_realize_target_graph_witness_output pfrep_right_realize_target_graph_witness_output. ((exists pfrep_position_realize_target_graph_witness_outputfirst. ((pfrep_position_realize_target_graph_witness_outputfirst+S (pfrep_power_realize_target_graph_witness_output)=(pfaa_length_realize_target_graph)) /\ ((((exists ff_h_pfp_realize_target_graph_witness_outputfirstentry. ff_h_pfp_realize_target_graph_witness_outputfirstentry + S (pfrep_left_realize_target_graph_witness_output) = S ((S (pfrep_position_realize_target_graph_witness_outputfirst)) * pfaa_sum_c_realize_target_graph)) /\ exists ff_q_pfp_realize_target_graph_witness_outputfirstentry. pfaa_sum_b_realize_target_graph = ff_q_pfp_realize_target_graph_witness_outputfirstentry * S ((S (pfrep_position_realize_target_graph_witness_outputfirst)) * pfaa_sum_c_realize_target_graph) + (pfrep_left_realize_target_graph_witness_output)))))) \/ (((exists pfrep_gap_realize_target_graph_witness_outputfirstoutside. pfrep_gap_realize_target_graph_witness_outputfirstoutside+(pfaa_length_realize_target_graph)=(pfrep_power_realize_target_graph_witness_output)) /\ (((pfrep_left_realize_target_graph_witness_output)=0))))) -> ((exists pfrep_position_realize_target_graph_witness_outputsecond. ((pfrep_position_realize_target_graph_witness_outputsecond+S (pfrep_power_realize_target_graph_witness_output)=(K)) /\ ((((exists ff_h_pfp_realize_target_graph_witness_outputsecondentry. ff_h_pfp_realize_target_graph_witness_outputsecondentry + S (pfrep_right_realize_target_graph_witness_output) = S ((S (pfrep_position_realize_target_graph_witness_outputsecond)) * tc)) /\ exists ff_q_pfp_realize_target_graph_witness_outputsecondentry. tb = ff_q_pfp_realize_target_graph_witness_outputsecondentry * S ((S (pfrep_position_realize_target_graph_witness_outputsecond)) * tc) + (pfrep_right_realize_target_graph_witness_output)))))) \/ (((exists pfrep_gap_realize_target_graph_witness_outputsecondoutside. pfrep_gap_realize_target_graph_witness_outputsecondoutside+(K)=(pfrep_power_realize_target_graph_witness_output)) /\ (((pfrep_right_realize_target_graph_witness_output)=0))))) -> pfrep_left_realize_target_graph_witness_output=pfrep_right_realize_target_graph_witness_output))))))))))))
  55. 0055specialize prime_field_polynomial_aligned_add_transport (p)
  56. 0056specialize prime_field_polynomial_aligned_add_transport (ab)
  57. 0057specialize prime_field_polynomial_aligned_add_transport (ac)
  58. 0058specialize prime_field_polynomial_aligned_add_transport (L)
  59. 0059specialize prime_field_polynomial_aligned_add_transport (bb)
  60. 0060specialize prime_field_polynomial_aligned_add_transport (bc)
  61. 0061specialize prime_field_polynomial_aligned_add_transport (M)
  62. 0062specialize prime_field_polynomial_aligned_add_transport (rb)
  63. 0063specialize prime_field_polynomial_aligned_add_transport (rc)
  64. 0064specialize prime_field_polynomial_aligned_add_transport (N)
  65. 0065specialize prime_field_polynomial_aligned_add_transport (ub)
  66. 0066specialize prime_field_polynomial_aligned_add_transport (uc)
  67. 0067specialize prime_field_polynomial_aligned_add_transport (K)
  68. 0068specialize prime_field_polynomial_aligned_add_transport (vb)
  69. 0069specialize prime_field_polynomial_aligned_add_transport (vc)
  70. 0070specialize prime_field_polynomial_aligned_add_transport (K)
  71. 0071specialize prime_field_polynomial_aligned_add_transport (tb)
  72. 0072specialize prime_field_polynomial_aligned_add_transport (tc)
  73. 0073specialize prime_field_polynomial_aligned_add_transport (K)
  74. 0074apply prime_field_polynomial_aligned_add_transport
  75. 0075exact hu
  76. 0076exact hv
  77. 0077exact ht
  78. 0078specialize prime_field_polynomial_equivalent_symmetric (ab)
  79. 0079specialize prime_field_polynomial_equivalent_symmetric (ac)
  80. 0080specialize prime_field_polynomial_equivalent_symmetric (L)
  81. 0081specialize prime_field_polynomial_equivalent_symmetric (ub)
  82. 0082specialize prime_field_polynomial_equivalent_symmetric (uc)
  83. 0083specialize prime_field_polynomial_equivalent_symmetric (K)
  84. 0084apply prime_field_polynomial_equivalent_symmetric
  85. 0085exact hc_left
  86. 0086specialize prime_field_polynomial_equivalent_symmetric (bb)
  87. 0087specialize prime_field_polynomial_equivalent_symmetric (bc)
  88. 0088specialize prime_field_polynomial_equivalent_symmetric (M)
  89. 0089specialize prime_field_polynomial_equivalent_symmetric (vb)
  90. 0090specialize prime_field_polynomial_equivalent_symmetric (vc)
  91. 0091specialize prime_field_polynomial_equivalent_symmetric (K)
  92. 0092apply prime_field_polynomial_equivalent_symmetric
  93. 0093exact hc_right
  94. 0094exact hr
  95. 0095exact h
  96. 0096have he : forall pfrep_power_realize_output_equivalent pfrep_left_realize_output_equivalent pfrep_right_realize_output_equivalent. ((exists pfrep_position_realize_output_equivalentfirst. ((pfrep_position_realize_output_equivalentfirst+S (pfrep_power_realize_output_equivalent)=(K)) /\ ((((exists ff_h_pfp_realize_output_equivalentfirstentry. ff_h_pfp_realize_output_equivalentfirstentry + S (pfrep_left_realize_output_equivalent) = S ((S (pfrep_position_realize_output_equivalentfirst)) * x1)) /\ exists ff_q_pfp_realize_output_equivalentfirstentry. x = ff_q_pfp_realize_output_equivalentfirstentry * S ((S (pfrep_position_realize_output_equivalentfirst)) * x1) + (pfrep_left_realize_output_equivalent)))))) \/ (((exists pfrep_gap_realize_output_equivalentfirstoutside. pfrep_gap_realize_output_equivalentfirstoutside+(K)=(pfrep_power_realize_output_equivalent)) /\ (((pfrep_left_realize_output_equivalent)=0))))) -> ((exists pfrep_position_realize_output_equivalentsecond. ((pfrep_position_realize_output_equivalentsecond+S (pfrep_power_realize_output_equivalent)=(K)) /\ ((((exists ff_h_pfp_realize_output_equivalentsecondentry. ff_h_pfp_realize_output_equivalentsecondentry + S (pfrep_right_realize_output_equivalent) = S ((S (pfrep_position_realize_output_equivalentsecond)) * tc)) /\ exists ff_q_pfp_realize_output_equivalentsecondentry. tb = ff_q_pfp_realize_output_equivalentsecondentry * S ((S (pfrep_position_realize_output_equivalentsecond)) * tc) + (pfrep_right_realize_output_equivalent)))))) \/ (((exists pfrep_gap_realize_output_equivalentsecondoutside. pfrep_gap_realize_output_equivalentsecondoutside+(K)=(pfrep_power_realize_output_equivalent)) /\ (((pfrep_right_realize_output_equivalent)=0))))) -> pfrep_left_realize_output_equivalent=pfrep_right_realize_output_equivalent
  97. 0097specialize prime_field_polynomial_aligned_add_functional (p)
  98. 0098specialize prime_field_polynomial_aligned_add_functional (ub)
  99. 0099specialize prime_field_polynomial_aligned_add_functional (uc)
  100. 0100specialize prime_field_polynomial_aligned_add_functional (K)
  101. 0101specialize prime_field_polynomial_aligned_add_functional (vb)
  102. 0102specialize prime_field_polynomial_aligned_add_functional (vc)
  103. 0103specialize prime_field_polynomial_aligned_add_functional (K)
  104. 0104specialize prime_field_polynomial_aligned_add_functional (x)
  105. 0105specialize prime_field_polynomial_aligned_add_functional (x1)
  106. 0106specialize prime_field_polynomial_aligned_add_functional (K)
  107. 0107specialize prime_field_polynomial_aligned_add_functional (tb)
  108. 0108specialize prime_field_polynomial_aligned_add_functional (tc)
  109. 0109specialize prime_field_polynomial_aligned_add_functional (K)
  110. 0110apply prime_field_polynomial_aligned_add_functional
  111. 0111exact hp
  112. 0112exact hzgraph
  113. 0113exact htgraph
  114. 0114specialize prime_field_polynomial_add_transport (p)
  115. 0115specialize prime_field_polynomial_add_transport (ub)
  116. 0116specialize prime_field_polynomial_add_transport (uc)
  117. 0117specialize prime_field_polynomial_add_transport (vb)
  118. 0118specialize prime_field_polynomial_add_transport (vc)
  119. 0119specialize prime_field_polynomial_add_transport (x)
  120. 0120specialize prime_field_polynomial_add_transport (x1)
  121. 0121specialize prime_field_polynomial_add_transport (ub)
  122. 0122specialize prime_field_polynomial_add_transport (uc)
  123. 0123specialize prime_field_polynomial_add_transport (vb)
  124. 0124specialize prime_field_polynomial_add_transport (vc)
  125. 0125specialize prime_field_polynomial_add_transport (tb)
  126. 0126specialize prime_field_polynomial_add_transport (tc)
  127. 0127specialize prime_field_polynomial_add_transport (K)
  128. 0128apply prime_field_polynomial_add_transport
  129. 0129intro i
  130. 0130intro a
  131. 0131intro hi
  132. 0132intro ha
  133. 0133exact ha
  134. 0134intro i
  135. 0135intro a
  136. 0136intro hi
  137. 0137intro ha
  138. 0138exact ha
  139. 0139specialize prime_field_polynomial_equivalent_implies_equal_same_length (x)
  140. 0140specialize prime_field_polynomial_equivalent_implies_equal_same_length (x1)
  141. 0141specialize prime_field_polynomial_equivalent_implies_equal_same_length (tb)
  142. 0142specialize prime_field_polynomial_equivalent_implies_equal_same_length (tc)
  143. 0143specialize prime_field_polynomial_equivalent_implies_equal_same_length (K)
  144. 0144apply prime_field_polynomial_equivalent_implies_equal_same_length
  145. 0145exact he
  146. 0146exact hz_witness_witness