PG0022

prime_field_polynomial_shift_scale_aligned_congruent

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

Formal equivalence of two old prefixes preserves every actual aligned sum of their trailing-zero shifts with a fixed actual scalar multiple of the same source. Both old lengths, all shift/scale encodings, both leading paddings and the sum encodings remain independent; only formal output coefficients are concluded equal.

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 c ab ac L b0 c0 N0 b1 c1 N1 u0b u0c v0b v0c UP0b UP0c VP0b VP0c z0b z0c u1b u1c v1b v1c UP1b UP1c VP1b VP1c z1b z1c. (~((p) = 1) /\ forall pfa_factor_left_step_alignment_prime pfa_factor_right_step_alignment_prime. (p) = pfa_factor_left_step_alignment_prime * pfa_factor_right_step_alignment_prime -> pfa_factor_left_step_alignment_prime = 1 \/ pfa_factor_right_step_alignment_prime = 1) -> (forall pfrep_power_step_alignment_old_equal pfrep_left_step_alignment_old_equal pfrep_right_step_alignment_old_equal. ((exists pfrep_position_step_alignment_old_equalfirst. ((pfrep_position_step_alignment_old_equalfirst+S (pfrep_power_step_alignment_old_equal)=(N0)) /\ ((((exists ff_h_pfp_step_alignment_old_equalfirstentry. ff_h_pfp_step_alignment_old_equalfirstentry + S (pfrep_left_step_alignment_old_equal) = S ((S (pfrep_position_step_alignment_old_equalfirst)) * c0)) /\ exists ff_q_pfp_step_alignment_old_equalfirstentry. b0 = ff_q_pfp_step_alignment_old_equalfirstentry * S ((S (pfrep_position_step_alignment_old_equalfirst)) * c0) + (pfrep_left_step_alignment_old_equal)))))) \/ (((exists pfrep_gap_step_alignment_old_equalfirstoutside. pfrep_gap_step_alignment_old_equalfirstoutside+(N0)=(pfrep_power_step_alignment_old_equal)) /\ (((pfrep_left_step_alignment_old_equal)=0))))) -> ((exists pfrep_position_step_alignment_old_equalsecond. ((pfrep_position_step_alignment_old_equalsecond+S (pfrep_power_step_alignment_old_equal)=(N1)) /\ ((((exists ff_h_pfp_step_alignment_old_equalsecondentry. ff_h_pfp_step_alignment_old_equalsecondentry + S (pfrep_right_step_alignment_old_equal) = S ((S (pfrep_position_step_alignment_old_equalsecond)) * c1)) /\ exists ff_q_pfp_step_alignment_old_equalsecondentry. b1 = ff_q_pfp_step_alignment_old_equalsecondentry * S ((S (pfrep_position_step_alignment_old_equalsecond)) * c1) + (pfrep_right_step_alignment_old_equal)))))) \/ (((exists pfrep_gap_step_alignment_old_equalsecondoutside. pfrep_gap_step_alignment_old_equalsecondoutside+(N1)=(pfrep_power_step_alignment_old_equal)) /\ (((pfrep_right_step_alignment_old_equal)=0))))) -> pfrep_left_step_alignment_old_equal=pfrep_right_step_alignment_old_equal) -> (((forall mdr_i_pfp_step_alignment_old_shiftprefix mdr_a_pfp_step_alignment_old_shiftprefix. (exists mdr_gap_pfp_step_alignment_old_shiftprefixb. mdr_gap_pfp_step_alignment_old_shiftprefixb + S (mdr_i_pfp_step_alignment_old_shiftprefix) = (N0)) -> (((exists ff_h_mdr_pfp_step_alignment_old_shiftprefixo. ff_h_mdr_pfp_step_alignment_old_shiftprefixo + S (mdr_a_pfp_step_alignment_old_shiftprefix) = S ((S (mdr_i_pfp_step_alignment_old_shiftprefix)) * c0)) /\ exists ff_q_mdr_pfp_step_alignment_old_shiftprefixo. b0 = ff_q_mdr_pfp_step_alignment_old_shiftprefixo * S ((S (mdr_i_pfp_step_alignment_old_shiftprefix)) * c0) + (mdr_a_pfp_step_alignment_old_shiftprefix))) -> (((exists ff_h_mdr_pfp_step_alignment_old_shiftprefixn. ff_h_mdr_pfp_step_alignment_old_shiftprefixn + S (mdr_a_pfp_step_alignment_old_shiftprefix) = S ((S (mdr_i_pfp_step_alignment_old_shiftprefix)) * u0c)) /\ exists ff_q_mdr_pfp_step_alignment_old_shiftprefixn. u0b = ff_q_mdr_pfp_step_alignment_old_shiftprefixn * S ((S (mdr_i_pfp_step_alignment_old_shiftprefix)) * u0c) + (mdr_a_pfp_step_alignment_old_shiftprefix)))) /\ ((((exists ff_h_pfp_step_alignment_old_shiftzero. ff_h_pfp_step_alignment_old_shiftzero + S (0) = S ((S (N0)) * u0c)) /\ exists ff_q_pfp_step_alignment_old_shiftzero. u0b = ff_q_pfp_step_alignment_old_shiftzero * S ((S (N0)) * u0c) + (0)))))) -> (((exists pfa_gap_step_alignment_old_scalescalar. pfa_gap_step_alignment_old_scalescalar + S (c) = (p)) /\ ((forall pfp_index_step_alignment_old_scale. (exists pfa_gap_step_alignment_old_scaleindex. pfa_gap_step_alignment_old_scaleindex + S (pfp_index_step_alignment_old_scale) = (L)) -> exists pfp_source_step_alignment_old_scale pfp_value_step_alignment_old_scale. ((((exists ff_h_pfp_step_alignment_old_scalesource. ff_h_pfp_step_alignment_old_scalesource + S (pfp_source_step_alignment_old_scale) = S ((S (pfp_index_step_alignment_old_scale)) * ac)) /\ exists ff_q_pfp_step_alignment_old_scalesource. ab = ff_q_pfp_step_alignment_old_scalesource * S ((S (pfp_index_step_alignment_old_scale)) * ac) + (pfp_source_step_alignment_old_scale))) /\ (((((exists ff_h_pfp_step_alignment_old_scaletarget. ff_h_pfp_step_alignment_old_scaletarget + S (pfp_value_step_alignment_old_scale) = S ((S (pfp_index_step_alignment_old_scale)) * v0c)) /\ exists ff_q_pfp_step_alignment_old_scaletarget. v0b = ff_q_pfp_step_alignment_old_scaletarget * S ((S (pfp_index_step_alignment_old_scale)) * v0c) + (pfp_value_step_alignment_old_scale))) /\ ((((exists pfa_gap_step_alignment_old_scaleoperationleft. pfa_gap_step_alignment_old_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_step_alignment_old_scaleoperationright. pfa_gap_step_alignment_old_scaleoperationright + S (pfp_source_step_alignment_old_scale) = (p)) /\ ((((exists pfa_gap_step_alignment_old_scaleoperationresultbound. pfa_gap_step_alignment_old_scaleoperationresultbound + S (pfp_value_step_alignment_old_scale) = (p)) /\ ((exists pfa_offset_left_step_alignment_old_scaleoperationresultcongruence pfa_offset_right_step_alignment_old_scaleoperationresultcongruence. ((c) * (pfp_source_step_alignment_old_scale)) + (p) * pfa_offset_left_step_alignment_old_scaleoperationresultcongruence = (pfp_value_step_alignment_old_scale) + (p) * pfa_offset_right_step_alignment_old_scaleoperationresultcongruence))))))))))))))))) -> (((forall pfp_repeat_index_step_alignment_old_leftzeros. (exists pfa_gap_step_alignment_old_leftzerosindex. pfa_gap_step_alignment_old_leftzerosindex + S (pfp_repeat_index_step_alignment_old_leftzeros) = (L)) -> (((exists ff_h_pfp_step_alignment_old_leftzerosentry. ff_h_pfp_step_alignment_old_leftzerosentry + S (0) = S ((S (pfp_repeat_index_step_alignment_old_leftzeros)) * UP0c)) /\ exists ff_q_pfp_step_alignment_old_leftzerosentry. UP0b = ff_q_pfp_step_alignment_old_leftzerosentry * S ((S (pfp_repeat_index_step_alignment_old_leftzeros)) * UP0c) + (0)))) /\ ((forall pfrep_index_step_alignment_old_left pfrep_value_step_alignment_old_left. (exists pfa_gap_step_alignment_old_leftbound. pfa_gap_step_alignment_old_leftbound + S (pfrep_index_step_alignment_old_left) = (S N0)) -> (((exists ff_h_pfp_step_alignment_old_leftinput. ff_h_pfp_step_alignment_old_leftinput + S (pfrep_value_step_alignment_old_left) = S ((S (pfrep_index_step_alignment_old_left)) * u0c)) /\ exists ff_q_pfp_step_alignment_old_leftinput. u0b = ff_q_pfp_step_alignment_old_leftinput * S ((S (pfrep_index_step_alignment_old_left)) * u0c) + (pfrep_value_step_alignment_old_left))) -> (((exists ff_h_pfp_step_alignment_old_leftoutput. ff_h_pfp_step_alignment_old_leftoutput + S (pfrep_value_step_alignment_old_left) = S ((S ((L)+pfrep_index_step_alignment_old_left)) * UP0c)) /\ exists ff_q_pfp_step_alignment_old_leftoutput. UP0b = ff_q_pfp_step_alignment_old_leftoutput * S ((S ((L)+pfrep_index_step_alignment_old_left)) * UP0c) + (pfrep_value_step_alignment_old_left))))))) -> (((forall pfp_repeat_index_step_alignment_old_rightzeros. (exists pfa_gap_step_alignment_old_rightzerosindex. pfa_gap_step_alignment_old_rightzerosindex + S (pfp_repeat_index_step_alignment_old_rightzeros) = (S N0)) -> (((exists ff_h_pfp_step_alignment_old_rightzerosentry. ff_h_pfp_step_alignment_old_rightzerosentry + S (0) = S ((S (pfp_repeat_index_step_alignment_old_rightzeros)) * VP0c)) /\ exists ff_q_pfp_step_alignment_old_rightzerosentry. VP0b = ff_q_pfp_step_alignment_old_rightzerosentry * S ((S (pfp_repeat_index_step_alignment_old_rightzeros)) * VP0c) + (0)))) /\ ((forall pfrep_index_step_alignment_old_right pfrep_value_step_alignment_old_right. (exists pfa_gap_step_alignment_old_rightbound. pfa_gap_step_alignment_old_rightbound + S (pfrep_index_step_alignment_old_right) = (L)) -> (((exists ff_h_pfp_step_alignment_old_rightinput. ff_h_pfp_step_alignment_old_rightinput + S (pfrep_value_step_alignment_old_right) = S ((S (pfrep_index_step_alignment_old_right)) * v0c)) /\ exists ff_q_pfp_step_alignment_old_rightinput. v0b = ff_q_pfp_step_alignment_old_rightinput * S ((S (pfrep_index_step_alignment_old_right)) * v0c) + (pfrep_value_step_alignment_old_right))) -> (((exists ff_h_pfp_step_alignment_old_rightoutput. ff_h_pfp_step_alignment_old_rightoutput + S (pfrep_value_step_alignment_old_right) = S ((S ((S N0)+pfrep_index_step_alignment_old_right)) * VP0c)) /\ exists ff_q_pfp_step_alignment_old_rightoutput. VP0b = ff_q_pfp_step_alignment_old_rightoutput * S ((S ((S N0)+pfrep_index_step_alignment_old_right)) * VP0c) + (pfrep_value_step_alignment_old_right))))))) -> (forall pfp_index_step_alignment_old_sum. (exists pfa_gap_step_alignment_old_sumindex. pfa_gap_step_alignment_old_sumindex + S (pfp_index_step_alignment_old_sum) = (L+S N0)) -> exists pfp_left_step_alignment_old_sum pfp_right_step_alignment_old_sum pfp_value_step_alignment_old_sum. ((((exists ff_h_pfp_step_alignment_old_sumleft. ff_h_pfp_step_alignment_old_sumleft + S (pfp_left_step_alignment_old_sum) = S ((S (pfp_index_step_alignment_old_sum)) * UP0c)) /\ exists ff_q_pfp_step_alignment_old_sumleft. UP0b = ff_q_pfp_step_alignment_old_sumleft * S ((S (pfp_index_step_alignment_old_sum)) * UP0c) + (pfp_left_step_alignment_old_sum))) /\ (((((exists ff_h_pfp_step_alignment_old_sumright. ff_h_pfp_step_alignment_old_sumright + S (pfp_right_step_alignment_old_sum) = S ((S (pfp_index_step_alignment_old_sum)) * VP0c)) /\ exists ff_q_pfp_step_alignment_old_sumright. VP0b = ff_q_pfp_step_alignment_old_sumright * S ((S (pfp_index_step_alignment_old_sum)) * VP0c) + (pfp_right_step_alignment_old_sum))) /\ (((((exists ff_h_pfp_step_alignment_old_sumtarget. ff_h_pfp_step_alignment_old_sumtarget + S (pfp_value_step_alignment_old_sum) = S ((S (pfp_index_step_alignment_old_sum)) * z0c)) /\ exists ff_q_pfp_step_alignment_old_sumtarget. z0b = ff_q_pfp_step_alignment_old_sumtarget * S ((S (pfp_index_step_alignment_old_sum)) * z0c) + (pfp_value_step_alignment_old_sum))) /\ ((((exists pfa_gap_step_alignment_old_sumoperationleft. pfa_gap_step_alignment_old_sumoperationleft + S (pfp_left_step_alignment_old_sum) = (p)) /\ (((exists pfa_gap_step_alignment_old_sumoperationright. pfa_gap_step_alignment_old_sumoperationright + S (pfp_right_step_alignment_old_sum) = (p)) /\ ((((exists pfa_gap_step_alignment_old_sumoperationresultbound. pfa_gap_step_alignment_old_sumoperationresultbound + S (pfp_value_step_alignment_old_sum) = (p)) /\ ((exists pfa_offset_left_step_alignment_old_sumoperationresultcongruence pfa_offset_right_step_alignment_old_sumoperationresultcongruence. ((pfp_left_step_alignment_old_sum) + (pfp_right_step_alignment_old_sum)) + (p) * pfa_offset_left_step_alignment_old_sumoperationresultcongruence = (pfp_value_step_alignment_old_sum) + (p) * pfa_offset_right_step_alignment_old_sumoperationresultcongruence)))))))))))))))) -> (((forall mdr_i_pfp_step_alignment_new_shiftprefix mdr_a_pfp_step_alignment_new_shiftprefix. (exists mdr_gap_pfp_step_alignment_new_shiftprefixb. mdr_gap_pfp_step_alignment_new_shiftprefixb + S (mdr_i_pfp_step_alignment_new_shiftprefix) = (N1)) -> (((exists ff_h_mdr_pfp_step_alignment_new_shiftprefixo. ff_h_mdr_pfp_step_alignment_new_shiftprefixo + S (mdr_a_pfp_step_alignment_new_shiftprefix) = S ((S (mdr_i_pfp_step_alignment_new_shiftprefix)) * c1)) /\ exists ff_q_mdr_pfp_step_alignment_new_shiftprefixo. b1 = ff_q_mdr_pfp_step_alignment_new_shiftprefixo * S ((S (mdr_i_pfp_step_alignment_new_shiftprefix)) * c1) + (mdr_a_pfp_step_alignment_new_shiftprefix))) -> (((exists ff_h_mdr_pfp_step_alignment_new_shiftprefixn. ff_h_mdr_pfp_step_alignment_new_shiftprefixn + S (mdr_a_pfp_step_alignment_new_shiftprefix) = S ((S (mdr_i_pfp_step_alignment_new_shiftprefix)) * u1c)) /\ exists ff_q_mdr_pfp_step_alignment_new_shiftprefixn. u1b = ff_q_mdr_pfp_step_alignment_new_shiftprefixn * S ((S (mdr_i_pfp_step_alignment_new_shiftprefix)) * u1c) + (mdr_a_pfp_step_alignment_new_shiftprefix)))) /\ ((((exists ff_h_pfp_step_alignment_new_shiftzero. ff_h_pfp_step_alignment_new_shiftzero + S (0) = S ((S (N1)) * u1c)) /\ exists ff_q_pfp_step_alignment_new_shiftzero. u1b = ff_q_pfp_step_alignment_new_shiftzero * S ((S (N1)) * u1c) + (0)))))) -> (((exists pfa_gap_step_alignment_new_scalescalar. pfa_gap_step_alignment_new_scalescalar + S (c) = (p)) /\ ((forall pfp_index_step_alignment_new_scale. (exists pfa_gap_step_alignment_new_scaleindex. pfa_gap_step_alignment_new_scaleindex + S (pfp_index_step_alignment_new_scale) = (L)) -> exists pfp_source_step_alignment_new_scale pfp_value_step_alignment_new_scale. ((((exists ff_h_pfp_step_alignment_new_scalesource. ff_h_pfp_step_alignment_new_scalesource + S (pfp_source_step_alignment_new_scale) = S ((S (pfp_index_step_alignment_new_scale)) * ac)) /\ exists ff_q_pfp_step_alignment_new_scalesource. ab = ff_q_pfp_step_alignment_new_scalesource * S ((S (pfp_index_step_alignment_new_scale)) * ac) + (pfp_source_step_alignment_new_scale))) /\ (((((exists ff_h_pfp_step_alignment_new_scaletarget. ff_h_pfp_step_alignment_new_scaletarget + S (pfp_value_step_alignment_new_scale) = S ((S (pfp_index_step_alignment_new_scale)) * v1c)) /\ exists ff_q_pfp_step_alignment_new_scaletarget. v1b = ff_q_pfp_step_alignment_new_scaletarget * S ((S (pfp_index_step_alignment_new_scale)) * v1c) + (pfp_value_step_alignment_new_scale))) /\ ((((exists pfa_gap_step_alignment_new_scaleoperationleft. pfa_gap_step_alignment_new_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_step_alignment_new_scaleoperationright. pfa_gap_step_alignment_new_scaleoperationright + S (pfp_source_step_alignment_new_scale) = (p)) /\ ((((exists pfa_gap_step_alignment_new_scaleoperationresultbound. pfa_gap_step_alignment_new_scaleoperationresultbound + S (pfp_value_step_alignment_new_scale) = (p)) /\ ((exists pfa_offset_left_step_alignment_new_scaleoperationresultcongruence pfa_offset_right_step_alignment_new_scaleoperationresultcongruence. ((c) * (pfp_source_step_alignment_new_scale)) + (p) * pfa_offset_left_step_alignment_new_scaleoperationresultcongruence = (pfp_value_step_alignment_new_scale) + (p) * pfa_offset_right_step_alignment_new_scaleoperationresultcongruence))))))))))))))))) -> (((forall pfp_repeat_index_step_alignment_new_leftzeros. (exists pfa_gap_step_alignment_new_leftzerosindex. pfa_gap_step_alignment_new_leftzerosindex + S (pfp_repeat_index_step_alignment_new_leftzeros) = (L)) -> (((exists ff_h_pfp_step_alignment_new_leftzerosentry. ff_h_pfp_step_alignment_new_leftzerosentry + S (0) = S ((S (pfp_repeat_index_step_alignment_new_leftzeros)) * UP1c)) /\ exists ff_q_pfp_step_alignment_new_leftzerosentry. UP1b = ff_q_pfp_step_alignment_new_leftzerosentry * S ((S (pfp_repeat_index_step_alignment_new_leftzeros)) * UP1c) + (0)))) /\ ((forall pfrep_index_step_alignment_new_left pfrep_value_step_alignment_new_left. (exists pfa_gap_step_alignment_new_leftbound. pfa_gap_step_alignment_new_leftbound + S (pfrep_index_step_alignment_new_left) = (S N1)) -> (((exists ff_h_pfp_step_alignment_new_leftinput. ff_h_pfp_step_alignment_new_leftinput + S (pfrep_value_step_alignment_new_left) = S ((S (pfrep_index_step_alignment_new_left)) * u1c)) /\ exists ff_q_pfp_step_alignment_new_leftinput. u1b = ff_q_pfp_step_alignment_new_leftinput * S ((S (pfrep_index_step_alignment_new_left)) * u1c) + (pfrep_value_step_alignment_new_left))) -> (((exists ff_h_pfp_step_alignment_new_leftoutput. ff_h_pfp_step_alignment_new_leftoutput + S (pfrep_value_step_alignment_new_left) = S ((S ((L)+pfrep_index_step_alignment_new_left)) * UP1c)) /\ exists ff_q_pfp_step_alignment_new_leftoutput. UP1b = ff_q_pfp_step_alignment_new_leftoutput * S ((S ((L)+pfrep_index_step_alignment_new_left)) * UP1c) + (pfrep_value_step_alignment_new_left))))))) -> (((forall pfp_repeat_index_step_alignment_new_rightzeros. (exists pfa_gap_step_alignment_new_rightzerosindex. pfa_gap_step_alignment_new_rightzerosindex + S (pfp_repeat_index_step_alignment_new_rightzeros) = (S N1)) -> (((exists ff_h_pfp_step_alignment_new_rightzerosentry. ff_h_pfp_step_alignment_new_rightzerosentry + S (0) = S ((S (pfp_repeat_index_step_alignment_new_rightzeros)) * VP1c)) /\ exists ff_q_pfp_step_alignment_new_rightzerosentry. VP1b = ff_q_pfp_step_alignment_new_rightzerosentry * S ((S (pfp_repeat_index_step_alignment_new_rightzeros)) * VP1c) + (0)))) /\ ((forall pfrep_index_step_alignment_new_right pfrep_value_step_alignment_new_right. (exists pfa_gap_step_alignment_new_rightbound. pfa_gap_step_alignment_new_rightbound + S (pfrep_index_step_alignment_new_right) = (L)) -> (((exists ff_h_pfp_step_alignment_new_rightinput. ff_h_pfp_step_alignment_new_rightinput + S (pfrep_value_step_alignment_new_right) = S ((S (pfrep_index_step_alignment_new_right)) * v1c)) /\ exists ff_q_pfp_step_alignment_new_rightinput. v1b = ff_q_pfp_step_alignment_new_rightinput * S ((S (pfrep_index_step_alignment_new_right)) * v1c) + (pfrep_value_step_alignment_new_right))) -> (((exists ff_h_pfp_step_alignment_new_rightoutput. ff_h_pfp_step_alignment_new_rightoutput + S (pfrep_value_step_alignment_new_right) = S ((S ((S N1)+pfrep_index_step_alignment_new_right)) * VP1c)) /\ exists ff_q_pfp_step_alignment_new_rightoutput. VP1b = ff_q_pfp_step_alignment_new_rightoutput * S ((S ((S N1)+pfrep_index_step_alignment_new_right)) * VP1c) + (pfrep_value_step_alignment_new_right))))))) -> (forall pfp_index_step_alignment_new_sum. (exists pfa_gap_step_alignment_new_sumindex. pfa_gap_step_alignment_new_sumindex + S (pfp_index_step_alignment_new_sum) = (L+S N1)) -> exists pfp_left_step_alignment_new_sum pfp_right_step_alignment_new_sum pfp_value_step_alignment_new_sum. ((((exists ff_h_pfp_step_alignment_new_sumleft. ff_h_pfp_step_alignment_new_sumleft + S (pfp_left_step_alignment_new_sum) = S ((S (pfp_index_step_alignment_new_sum)) * UP1c)) /\ exists ff_q_pfp_step_alignment_new_sumleft. UP1b = ff_q_pfp_step_alignment_new_sumleft * S ((S (pfp_index_step_alignment_new_sum)) * UP1c) + (pfp_left_step_alignment_new_sum))) /\ (((((exists ff_h_pfp_step_alignment_new_sumright. ff_h_pfp_step_alignment_new_sumright + S (pfp_right_step_alignment_new_sum) = S ((S (pfp_index_step_alignment_new_sum)) * VP1c)) /\ exists ff_q_pfp_step_alignment_new_sumright. VP1b = ff_q_pfp_step_alignment_new_sumright * S ((S (pfp_index_step_alignment_new_sum)) * VP1c) + (pfp_right_step_alignment_new_sum))) /\ (((((exists ff_h_pfp_step_alignment_new_sumtarget. ff_h_pfp_step_alignment_new_sumtarget + S (pfp_value_step_alignment_new_sum) = S ((S (pfp_index_step_alignment_new_sum)) * z1c)) /\ exists ff_q_pfp_step_alignment_new_sumtarget. z1b = ff_q_pfp_step_alignment_new_sumtarget * S ((S (pfp_index_step_alignment_new_sum)) * z1c) + (pfp_value_step_alignment_new_sum))) /\ ((((exists pfa_gap_step_alignment_new_sumoperationleft. pfa_gap_step_alignment_new_sumoperationleft + S (pfp_left_step_alignment_new_sum) = (p)) /\ (((exists pfa_gap_step_alignment_new_sumoperationright. pfa_gap_step_alignment_new_sumoperationright + S (pfp_right_step_alignment_new_sum) = (p)) /\ ((((exists pfa_gap_step_alignment_new_sumoperationresultbound. pfa_gap_step_alignment_new_sumoperationresultbound + S (pfp_value_step_alignment_new_sum) = (p)) /\ ((exists pfa_offset_left_step_alignment_new_sumoperationresultcongruence pfa_offset_right_step_alignment_new_sumoperationresultcongruence. ((pfp_left_step_alignment_new_sum) + (pfp_right_step_alignment_new_sum)) + (p) * pfa_offset_left_step_alignment_new_sumoperationresultcongruence = (pfp_value_step_alignment_new_sum) + (p) * pfa_offset_right_step_alignment_new_sumoperationresultcongruence)))))))))))))))) -> (forall pfrep_power_step_alignment_result pfrep_left_step_alignment_result pfrep_right_step_alignment_result. ((exists pfrep_position_step_alignment_resultfirst. ((pfrep_position_step_alignment_resultfirst+S (pfrep_power_step_alignment_result)=(L+S N0)) /\ ((((exists ff_h_pfp_step_alignment_resultfirstentry. ff_h_pfp_step_alignment_resultfirstentry + S (pfrep_left_step_alignment_result) = S ((S (pfrep_position_step_alignment_resultfirst)) * z0c)) /\ exists ff_q_pfp_step_alignment_resultfirstentry. z0b = ff_q_pfp_step_alignment_resultfirstentry * S ((S (pfrep_position_step_alignment_resultfirst)) * z0c) + (pfrep_left_step_alignment_result)))))) \/ (((exists pfrep_gap_step_alignment_resultfirstoutside. pfrep_gap_step_alignment_resultfirstoutside+(L+S N0)=(pfrep_power_step_alignment_result)) /\ (((pfrep_left_step_alignment_result)=0))))) -> ((exists pfrep_position_step_alignment_resultsecond. ((pfrep_position_step_alignment_resultsecond+S (pfrep_power_step_alignment_result)=(L+S N1)) /\ ((((exists ff_h_pfp_step_alignment_resultsecondentry. ff_h_pfp_step_alignment_resultsecondentry + S (pfrep_right_step_alignment_result) = S ((S (pfrep_position_step_alignment_resultsecond)) * z1c)) /\ exists ff_q_pfp_step_alignment_resultsecondentry. z1b = ff_q_pfp_step_alignment_resultsecondentry * S ((S (pfrep_position_step_alignment_resultsecond)) * z1c) + (pfrep_right_step_alignment_result)))))) \/ (((exists pfrep_gap_step_alignment_resultsecondoutside. pfrep_gap_step_alignment_resultsecondoutside+(L+S N1)=(pfrep_power_step_alignment_result)) /\ (((pfrep_right_step_alignment_result)=0))))) -> pfrep_left_step_alignment_result=pfrep_right_step_alignment_result)

Constructive proof overview

Generated structural guide

Formal equivalence of two old prefixes preserves every actual aligned sum of their trailing-zero shifts with a fixed actual scalar multiple of the same source. Both old lengths, all shift/scale encodings, both leading paddings and the sum encodings remain independent; only formal output coefficients are concluded equal.

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

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

Proof neighborhood

Direct dependencies

PG0020 prime_field_polynomial_shift_equivalent_congruent prime_field_polynomial_scale_functional Alpha theorem; checked-use authorized prime_field_polynomial_equal_implies_equivalent Alpha theorem; checked-use authorized prime_field_polynomial_left_pad_equivalent Alpha theorem; checked-use authorized add_comm Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_transitive Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_symmetric Alpha theorem; checked-use authorized prime_field_polynomial_add_equivalent_congruent Alpha theorem; checked-use authorized

Direct dependents

PG0023 prime_field_polynomial_convolution_associativity_append_step

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

214 script commands · 26 reading checkpoints · 13 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 shift equivalent congruent

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 c
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro L
  6. L6
    intro b0
  7. L7
    intro c0
  8. L8
    intro N0
  9. L9
    intro b1
  10. L10
    intro c1
02Fix variables and assumptionsL11–20

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

  1. L11
    intro N1
  2. L12
    intro u0b
  3. L13
    intro u0c
  4. L14
    intro v0b
  5. L15
    intro v0c
  6. L16
    intro UP0b
  7. L17
    intro UP0c
  8. L18
    intro VP0b
  9. L19
    intro VP0c
  10. L20
    intro z0b
03Fix variables and assumptionsL21–30

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

  1. L21
    intro z0c
  2. L22
    intro u1b
  3. L23
    intro u1c
  4. L24
    intro v1b
  5. L25
    intro v1c
  6. L26
    intro UP1b
  7. L27
    intro UP1c
  8. L28
    intro VP1b
  9. L29
    intro VP1c
  10. L30
    intro z1b
04Fix variables and assumptionsL31–40

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

  1. L31
    intro z1c
  2. L32
    intro hp
  3. L33
    intro he
  4. L34
    intro hU0
  5. L35
    intro hV0
  6. L36
    intro hUP0
  7. L37
    intro hVP0
  8. L38
    intro hZ0
  9. L39
    intro hU1
  10. L40
    intro hV1
05Fix variables and assumptionsL41–43

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

  1. L41
    intro hUP1
  2. L42
    intro hVP1
  3. L43
    intro hZ1
06Establish hshiftedL44–53

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

  1. L44
    have hshifted : PolynomialEquivalent(u0b,u0c,S N0,u1b,u1c,S N1)Definitions: PolynomialEquivalent
  2. L45
    specialize prime_field_polynomial_shift_equivalent_congruent (b0)
  3. L46
    specialize prime_field_polynomial_shift_equivalent_congruent (c0)
  4. L47
    specialize prime_field_polynomial_shift_equivalent_congruent (N0)
  5. L48
    specialize prime_field_polynomial_shift_equivalent_congruent (b1)
  6. L49
    specialize prime_field_polynomial_shift_equivalent_congruent (c1)
  7. L50
    specialize prime_field_polynomial_shift_equivalent_congruent (N1)
  8. L51
    specialize prime_field_polynomial_shift_equivalent_congruent (u0b)
  9. L52
    specialize prime_field_polynomial_shift_equivalent_congruent (u0c)
  10. L53
    specialize prime_field_polynomial_shift_equivalent_congruent (u1b)
07Use earlier factsL54–58

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

  1. L54
    specialize prime_field_polynomial_shift_equivalent_congruent (u1c)
  2. L55
    apply prime_field_polynomial_shift_equivalent_congruent
  3. L56
    exact he
  4. L57
    exact hU0
  5. L58
    exact hU1
08Establish hscaledL59–68

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

  1. L59
    have hscaled : BetaPrefixEqual(v0b,v0c,v1b,v1c,L)Definitions: BetaPrefixEqual
  2. L60
    specialize prime_field_polynomial_scale_functional (p)
  3. L61
    specialize prime_field_polynomial_scale_functional (c)
  4. L62
    specialize prime_field_polynomial_scale_functional (ab)
  5. L63
    specialize prime_field_polynomial_scale_functional (ac)
  6. L64
    specialize prime_field_polynomial_scale_functional (v0b)
  7. L65
    specialize prime_field_polynomial_scale_functional (v0c)
  8. L66
    specialize prime_field_polynomial_scale_functional (v1b)
  9. L67
    specialize prime_field_polynomial_scale_functional (v1c)
  10. L68
    specialize prime_field_polynomial_scale_functional (L)
09Use earlier factsL69–71

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

  1. L69
    apply prime_field_polynomial_scale_functional
  2. L70
    exact hV0
  3. L71
    exact hV1
10Establish hscalar_equalL72–79

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

  1. L72
    have hscalar_equal : PolynomialEquivalent(v0b,v0c,L,v1b,v1c,L)Definitions: PolynomialEquivalent
  2. L73
    specialize prime_field_polynomial_equal_implies_equivalent (v0b)
  3. L74
    specialize prime_field_polynomial_equal_implies_equivalent (v0c)
  4. L75
    specialize prime_field_polynomial_equal_implies_equivalent (v1b)
  5. L76
    specialize prime_field_polynomial_equal_implies_equivalent (v1c)
  6. L77
    specialize prime_field_polynomial_equal_implies_equivalent (L)
  7. L78
    apply prime_field_polynomial_equal_implies_equivalent
  8. L79
    exact hscaled
11Establish hpad_left0L80–88

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

  1. L80
    have hpad_left0 : PolynomialEquivalent(u0b,u0c,S N0,UP0b,UP0c,L + S N0)Definitions: PolynomialEquivalent
  2. L81
    specialize prime_field_polynomial_left_pad_equivalent (u0b)
  3. L82
    specialize prime_field_polynomial_left_pad_equivalent (u0c)
  4. L83
    specialize prime_field_polynomial_left_pad_equivalent (S N0)
  5. L84
    specialize prime_field_polynomial_left_pad_equivalent (L)
  6. L85
    specialize prime_field_polynomial_left_pad_equivalent (UP0b)
  7. L86
    specialize prime_field_polynomial_left_pad_equivalent (UP0c)
  8. L87
    apply prime_field_polynomial_left_pad_equivalent
  9. L88
    exact hUP0
12Establish hpad_left1L89–97

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

  1. L89
    have hpad_left1 : PolynomialEquivalent(u1b,u1c,S N1,UP1b,UP1c,L + S N1)Definitions: PolynomialEquivalent
  2. L90
    specialize prime_field_polynomial_left_pad_equivalent (u1b)
  3. L91
    specialize prime_field_polynomial_left_pad_equivalent (u1c)
  4. L92
    specialize prime_field_polynomial_left_pad_equivalent (S N1)
  5. L93
    specialize prime_field_polynomial_left_pad_equivalent (L)
  6. L94
    specialize prime_field_polynomial_left_pad_equivalent (UP1b)
  7. L95
    specialize prime_field_polynomial_left_pad_equivalent (UP1c)
  8. L96
    apply prime_field_polynomial_left_pad_equivalent
  9. L97
    exact hUP1
13Establish hpad_right0L98–106

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

  1. L98
    have hpad_right0 : PolynomialEquivalent(v0b,v0c,L,VP0b,VP0c,S N0 + L)Definitions: PolynomialEquivalent
  2. L99
    specialize prime_field_polynomial_left_pad_equivalent (v0b)
  3. L100
    specialize prime_field_polynomial_left_pad_equivalent (v0c)
  4. L101
    specialize prime_field_polynomial_left_pad_equivalent (L)
  5. L102
    specialize prime_field_polynomial_left_pad_equivalent (S N0)
  6. L103
    specialize prime_field_polynomial_left_pad_equivalent (VP0b)
  7. L104
    specialize prime_field_polynomial_left_pad_equivalent (VP0c)
  8. L105
    apply prime_field_polynomial_left_pad_equivalent
  9. L106
    exact hVP0
14Establish hcomm_right0L107–112

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

  1. L107
    have hcomm_right0 : S N0+L=L+S N0
  2. L108
    specialize add_comm (S N0)
  3. L109
    specialize add_comm (L)
  4. L110
    apply add_comm
  5. L111
    rewrite hcomm_right0 at hpad_right0
  6. L112
    rewrite hcomm_right0 at hpad_right0
15Establish hpad_right1L113–121

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

  1. L113
    have hpad_right1 : PolynomialEquivalent(v1b,v1c,L,VP1b,VP1c,S N1 + L)Definitions: PolynomialEquivalent
  2. L114
    specialize prime_field_polynomial_left_pad_equivalent (v1b)
  3. L115
    specialize prime_field_polynomial_left_pad_equivalent (v1c)
  4. L116
    specialize prime_field_polynomial_left_pad_equivalent (L)
  5. L117
    specialize prime_field_polynomial_left_pad_equivalent (S N1)
  6. L118
    specialize prime_field_polynomial_left_pad_equivalent (VP1b)
  7. L119
    specialize prime_field_polynomial_left_pad_equivalent (VP1c)
  8. L120
    apply prime_field_polynomial_left_pad_equivalent
  9. L121
    exact hVP1
16Establish hcomm_right1L122–127

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

  1. L122
    have hcomm_right1 : S N1+L=L+S N1
  2. L123
    specialize add_comm (S N1)
  3. L124
    specialize add_comm (L)
  4. L125
    apply add_comm
  5. L126
    rewrite hcomm_right1 at hpad_right1
  6. L127
    rewrite hcomm_right1 at hpad_right1
17Establish hmiddle_leftL128–137

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

  1. L128
    have hmiddle_left : PolynomialEquivalent(UP0b,UP0c,L + S N0,u1b,u1c,S N1)Definitions: PolynomialEquivalent
  2. L129
    specialize prime_field_polynomial_equivalent_transitive (UP0b)
  3. L130
    specialize prime_field_polynomial_equivalent_transitive (UP0c)
  4. L131
    specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  5. L132
    specialize prime_field_polynomial_equivalent_transitive (u0b)
  6. L133
    specialize prime_field_polynomial_equivalent_transitive (u0c)
  7. L134
    specialize prime_field_polynomial_equivalent_transitive (S N0)
  8. L135
    specialize prime_field_polynomial_equivalent_transitive (u1b)
  9. L136
    specialize prime_field_polynomial_equivalent_transitive (u1c)
  10. L137
    specialize prime_field_polynomial_equivalent_transitive (S N1)
18Use earlier factsL138–147

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

  1. L138
    apply prime_field_polynomial_equivalent_transitive
  2. L139
    specialize prime_field_polynomial_equivalent_symmetric (u0b)
  3. L140
    specialize prime_field_polynomial_equivalent_symmetric (u0c)
  4. L141
    specialize prime_field_polynomial_equivalent_symmetric (S N0)
  5. L142
    specialize prime_field_polynomial_equivalent_symmetric (UP0b)
  6. L143
    specialize prime_field_polynomial_equivalent_symmetric (UP0c)
  7. L144
    specialize prime_field_polynomial_equivalent_symmetric (L+S N0)
  8. L145
    apply prime_field_polynomial_equivalent_symmetric
  9. L146
    exact hpad_left0
  10. L147
    exact hshifted
19Establish hequal_leftL148–157

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

  1. L148
    have hequal_left : PolynomialEquivalent(UP0b,UP0c,L + S N0,UP1b,UP1c,L + S N1)Definitions: PolynomialEquivalent
  2. L149
    specialize prime_field_polynomial_equivalent_transitive (UP0b)
  3. L150
    specialize prime_field_polynomial_equivalent_transitive (UP0c)
  4. L151
    specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  5. L152
    specialize prime_field_polynomial_equivalent_transitive (u1b)
  6. L153
    specialize prime_field_polynomial_equivalent_transitive (u1c)
  7. L154
    specialize prime_field_polynomial_equivalent_transitive (S N1)
  8. L155
    specialize prime_field_polynomial_equivalent_transitive (UP1b)
  9. L156
    specialize prime_field_polynomial_equivalent_transitive (UP1c)
  10. L157
    specialize prime_field_polynomial_equivalent_transitive (L+S N1)
20Use earlier factsL158–160

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

  1. L158
    apply prime_field_polynomial_equivalent_transitive
  2. L159
    exact hmiddle_left
  3. L160
    exact hpad_left1
21Establish hmiddle_rightL161–170

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

  1. L161
    have hmiddle_right : PolynomialEquivalent(VP0b,VP0c,L + S N0,v1b,v1c,L)Definitions: PolynomialEquivalent
  2. L162
    specialize prime_field_polynomial_equivalent_transitive (VP0b)
  3. L163
    specialize prime_field_polynomial_equivalent_transitive (VP0c)
  4. L164
    specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  5. L165
    specialize prime_field_polynomial_equivalent_transitive (v0b)
  6. L166
    specialize prime_field_polynomial_equivalent_transitive (v0c)
  7. L167
    specialize prime_field_polynomial_equivalent_transitive (L)
  8. L168
    specialize prime_field_polynomial_equivalent_transitive (v1b)
  9. L169
    specialize prime_field_polynomial_equivalent_transitive (v1c)
  10. L170
    specialize prime_field_polynomial_equivalent_transitive (L)
22Use earlier factsL171–180

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

  1. L171
    apply prime_field_polynomial_equivalent_transitive
  2. L172
    specialize prime_field_polynomial_equivalent_symmetric (v0b)
  3. L173
    specialize prime_field_polynomial_equivalent_symmetric (v0c)
  4. L174
    specialize prime_field_polynomial_equivalent_symmetric (L)
  5. L175
    specialize prime_field_polynomial_equivalent_symmetric (VP0b)
  6. L176
    specialize prime_field_polynomial_equivalent_symmetric (VP0c)
  7. L177
    specialize prime_field_polynomial_equivalent_symmetric (L+S N0)
  8. L178
    apply prime_field_polynomial_equivalent_symmetric
  9. L179
    exact hpad_right0
  10. L180
    exact hscalar_equal
23Establish hequal_rightL181–190

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

  1. L181
    have hequal_right : PolynomialEquivalent(VP0b,VP0c,L + S N0,VP1b,VP1c,L + S N1)Definitions: PolynomialEquivalent
  2. L182
    specialize prime_field_polynomial_equivalent_transitive (VP0b)
  3. L183
    specialize prime_field_polynomial_equivalent_transitive (VP0c)
  4. L184
    specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  5. L185
    specialize prime_field_polynomial_equivalent_transitive (v1b)
  6. L186
    specialize prime_field_polynomial_equivalent_transitive (v1c)
  7. L187
    specialize prime_field_polynomial_equivalent_transitive (L)
  8. L188
    specialize prime_field_polynomial_equivalent_transitive (VP1b)
  9. L189
    specialize prime_field_polynomial_equivalent_transitive (VP1c)
  10. L190
    specialize prime_field_polynomial_equivalent_transitive (L+S N1)
24Use earlier factsL191–200

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

  1. L191
    apply prime_field_polynomial_equivalent_transitive
  2. L192
    exact hmiddle_right
  3. L193
    exact hpad_right1
  4. L194
    specialize prime_field_polynomial_add_equivalent_congruent (p)
  5. L195
    specialize prime_field_polynomial_add_equivalent_congruent (UP0b)
  6. L196
    specialize prime_field_polynomial_add_equivalent_congruent (UP0c)
  7. L197
    specialize prime_field_polynomial_add_equivalent_congruent (VP0b)
  8. L198
    specialize prime_field_polynomial_add_equivalent_congruent (VP0c)
  9. L199
    specialize prime_field_polynomial_add_equivalent_congruent (z0b)
  10. L200
    specialize prime_field_polynomial_add_equivalent_congruent (z0c)
25Use earlier factsL201–210

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

  1. L201
    specialize prime_field_polynomial_add_equivalent_congruent (L+S N0)
  2. L202
    specialize prime_field_polynomial_add_equivalent_congruent (UP1b)
  3. L203
    specialize prime_field_polynomial_add_equivalent_congruent (UP1c)
  4. L204
    specialize prime_field_polynomial_add_equivalent_congruent (VP1b)
  5. L205
    specialize prime_field_polynomial_add_equivalent_congruent (VP1c)
  6. L206
    specialize prime_field_polynomial_add_equivalent_congruent (z1b)
  7. L207
    specialize prime_field_polynomial_add_equivalent_congruent (z1c)
  8. L208
    specialize prime_field_polynomial_add_equivalent_congruent (L+S N1)
  9. L209
    apply prime_field_polynomial_add_equivalent_congruent
  10. L210
    exact hp
26Use earlier factsL211–214

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

  1. L211
    exact hequal_left
  2. L212
    exact hequal_right
  3. L213
    exact hZ0
  4. L214
    exact hZ1

Library-wide reading audit

Original exact command ledger · 214 lines
  1. 0001intro p
  2. 0002intro c
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro L
  6. 0006intro b0
  7. 0007intro c0
  8. 0008intro N0
  9. 0009intro b1
  10. 0010intro c1
  11. 0011intro N1
  12. 0012intro u0b
  13. 0013intro u0c
  14. 0014intro v0b
  15. 0015intro v0c
  16. 0016intro UP0b
  17. 0017intro UP0c
  18. 0018intro VP0b
  19. 0019intro VP0c
  20. 0020intro z0b
  21. 0021intro z0c
  22. 0022intro u1b
  23. 0023intro u1c
  24. 0024intro v1b
  25. 0025intro v1c
  26. 0026intro UP1b
  27. 0027intro UP1c
  28. 0028intro VP1b
  29. 0029intro VP1c
  30. 0030intro z1b
  31. 0031intro z1c
  32. 0032intro hp
  33. 0033intro he
  34. 0034intro hU0
  35. 0035intro hV0
  36. 0036intro hUP0
  37. 0037intro hVP0
  38. 0038intro hZ0
  39. 0039intro hU1
  40. 0040intro hV1
  41. 0041intro hUP1
  42. 0042intro hVP1
  43. 0043intro hZ1
  44. 0044have hshifted : forall pfrep_power_step_alignment_shifted pfrep_left_step_alignment_shifted pfrep_right_step_alignment_shifted. ((exists pfrep_position_step_alignment_shiftedfirst. ((pfrep_position_step_alignment_shiftedfirst+S (pfrep_power_step_alignment_shifted)=(S N0)) /\ ((((exists ff_h_pfp_step_alignment_shiftedfirstentry. ff_h_pfp_step_alignment_shiftedfirstentry + S (pfrep_left_step_alignment_shifted) = S ((S (pfrep_position_step_alignment_shiftedfirst)) * u0c)) /\ exists ff_q_pfp_step_alignment_shiftedfirstentry. u0b = ff_q_pfp_step_alignment_shiftedfirstentry * S ((S (pfrep_position_step_alignment_shiftedfirst)) * u0c) + (pfrep_left_step_alignment_shifted)))))) \/ (((exists pfrep_gap_step_alignment_shiftedfirstoutside. pfrep_gap_step_alignment_shiftedfirstoutside+(S N0)=(pfrep_power_step_alignment_shifted)) /\ (((pfrep_left_step_alignment_shifted)=0))))) -> ((exists pfrep_position_step_alignment_shiftedsecond. ((pfrep_position_step_alignment_shiftedsecond+S (pfrep_power_step_alignment_shifted)=(S N1)) /\ ((((exists ff_h_pfp_step_alignment_shiftedsecondentry. ff_h_pfp_step_alignment_shiftedsecondentry + S (pfrep_right_step_alignment_shifted) = S ((S (pfrep_position_step_alignment_shiftedsecond)) * u1c)) /\ exists ff_q_pfp_step_alignment_shiftedsecondentry. u1b = ff_q_pfp_step_alignment_shiftedsecondentry * S ((S (pfrep_position_step_alignment_shiftedsecond)) * u1c) + (pfrep_right_step_alignment_shifted)))))) \/ (((exists pfrep_gap_step_alignment_shiftedsecondoutside. pfrep_gap_step_alignment_shiftedsecondoutside+(S N1)=(pfrep_power_step_alignment_shifted)) /\ (((pfrep_right_step_alignment_shifted)=0))))) -> pfrep_left_step_alignment_shifted=pfrep_right_step_alignment_shifted
  45. 0045specialize prime_field_polynomial_shift_equivalent_congruent (b0)
  46. 0046specialize prime_field_polynomial_shift_equivalent_congruent (c0)
  47. 0047specialize prime_field_polynomial_shift_equivalent_congruent (N0)
  48. 0048specialize prime_field_polynomial_shift_equivalent_congruent (b1)
  49. 0049specialize prime_field_polynomial_shift_equivalent_congruent (c1)
  50. 0050specialize prime_field_polynomial_shift_equivalent_congruent (N1)
  51. 0051specialize prime_field_polynomial_shift_equivalent_congruent (u0b)
  52. 0052specialize prime_field_polynomial_shift_equivalent_congruent (u0c)
  53. 0053specialize prime_field_polynomial_shift_equivalent_congruent (u1b)
  54. 0054specialize prime_field_polynomial_shift_equivalent_congruent (u1c)
  55. 0055apply prime_field_polynomial_shift_equivalent_congruent
  56. 0056exact he
  57. 0057exact hU0
  58. 0058exact hU1
  59. 0059have hscaled : forall mdr_i_pfp_step_alignment_scaled mdr_a_pfp_step_alignment_scaled. (exists mdr_gap_pfp_step_alignment_scaledb. mdr_gap_pfp_step_alignment_scaledb + S (mdr_i_pfp_step_alignment_scaled) = (L)) -> (((exists ff_h_mdr_pfp_step_alignment_scaledo. ff_h_mdr_pfp_step_alignment_scaledo + S (mdr_a_pfp_step_alignment_scaled) = S ((S (mdr_i_pfp_step_alignment_scaled)) * v0c)) /\ exists ff_q_mdr_pfp_step_alignment_scaledo. v0b = ff_q_mdr_pfp_step_alignment_scaledo * S ((S (mdr_i_pfp_step_alignment_scaled)) * v0c) + (mdr_a_pfp_step_alignment_scaled))) -> (((exists ff_h_mdr_pfp_step_alignment_scaledn. ff_h_mdr_pfp_step_alignment_scaledn + S (mdr_a_pfp_step_alignment_scaled) = S ((S (mdr_i_pfp_step_alignment_scaled)) * v1c)) /\ exists ff_q_mdr_pfp_step_alignment_scaledn. v1b = ff_q_mdr_pfp_step_alignment_scaledn * S ((S (mdr_i_pfp_step_alignment_scaled)) * v1c) + (mdr_a_pfp_step_alignment_scaled)))
  60. 0060specialize prime_field_polynomial_scale_functional (p)
  61. 0061specialize prime_field_polynomial_scale_functional (c)
  62. 0062specialize prime_field_polynomial_scale_functional (ab)
  63. 0063specialize prime_field_polynomial_scale_functional (ac)
  64. 0064specialize prime_field_polynomial_scale_functional (v0b)
  65. 0065specialize prime_field_polynomial_scale_functional (v0c)
  66. 0066specialize prime_field_polynomial_scale_functional (v1b)
  67. 0067specialize prime_field_polynomial_scale_functional (v1c)
  68. 0068specialize prime_field_polynomial_scale_functional (L)
  69. 0069apply prime_field_polynomial_scale_functional
  70. 0070exact hV0
  71. 0071exact hV1
  72. 0072have hscalar_equal : forall pfrep_power_step_alignment_scalar_equal pfrep_left_step_alignment_scalar_equal pfrep_right_step_alignment_scalar_equal. ((exists pfrep_position_step_alignment_scalar_equalfirst. ((pfrep_position_step_alignment_scalar_equalfirst+S (pfrep_power_step_alignment_scalar_equal)=(L)) /\ ((((exists ff_h_pfp_step_alignment_scalar_equalfirstentry. ff_h_pfp_step_alignment_scalar_equalfirstentry + S (pfrep_left_step_alignment_scalar_equal) = S ((S (pfrep_position_step_alignment_scalar_equalfirst)) * v0c)) /\ exists ff_q_pfp_step_alignment_scalar_equalfirstentry. v0b = ff_q_pfp_step_alignment_scalar_equalfirstentry * S ((S (pfrep_position_step_alignment_scalar_equalfirst)) * v0c) + (pfrep_left_step_alignment_scalar_equal)))))) \/ (((exists pfrep_gap_step_alignment_scalar_equalfirstoutside. pfrep_gap_step_alignment_scalar_equalfirstoutside+(L)=(pfrep_power_step_alignment_scalar_equal)) /\ (((pfrep_left_step_alignment_scalar_equal)=0))))) -> ((exists pfrep_position_step_alignment_scalar_equalsecond. ((pfrep_position_step_alignment_scalar_equalsecond+S (pfrep_power_step_alignment_scalar_equal)=(L)) /\ ((((exists ff_h_pfp_step_alignment_scalar_equalsecondentry. ff_h_pfp_step_alignment_scalar_equalsecondentry + S (pfrep_right_step_alignment_scalar_equal) = S ((S (pfrep_position_step_alignment_scalar_equalsecond)) * v1c)) /\ exists ff_q_pfp_step_alignment_scalar_equalsecondentry. v1b = ff_q_pfp_step_alignment_scalar_equalsecondentry * S ((S (pfrep_position_step_alignment_scalar_equalsecond)) * v1c) + (pfrep_right_step_alignment_scalar_equal)))))) \/ (((exists pfrep_gap_step_alignment_scalar_equalsecondoutside. pfrep_gap_step_alignment_scalar_equalsecondoutside+(L)=(pfrep_power_step_alignment_scalar_equal)) /\ (((pfrep_right_step_alignment_scalar_equal)=0))))) -> pfrep_left_step_alignment_scalar_equal=pfrep_right_step_alignment_scalar_equal
  73. 0073specialize prime_field_polynomial_equal_implies_equivalent (v0b)
  74. 0074specialize prime_field_polynomial_equal_implies_equivalent (v0c)
  75. 0075specialize prime_field_polynomial_equal_implies_equivalent (v1b)
  76. 0076specialize prime_field_polynomial_equal_implies_equivalent (v1c)
  77. 0077specialize prime_field_polynomial_equal_implies_equivalent (L)
  78. 0078apply prime_field_polynomial_equal_implies_equivalent
  79. 0079exact hscaled
  80. 0080have hpad_left0 : forall pfrep_power_step_alignment_pad_left0 pfrep_left_step_alignment_pad_left0 pfrep_right_step_alignment_pad_left0. ((exists pfrep_position_step_alignment_pad_left0first. ((pfrep_position_step_alignment_pad_left0first+S (pfrep_power_step_alignment_pad_left0)=(S N0)) /\ ((((exists ff_h_pfp_step_alignment_pad_left0firstentry. ff_h_pfp_step_alignment_pad_left0firstentry + S (pfrep_left_step_alignment_pad_left0) = S ((S (pfrep_position_step_alignment_pad_left0first)) * u0c)) /\ exists ff_q_pfp_step_alignment_pad_left0firstentry. u0b = ff_q_pfp_step_alignment_pad_left0firstentry * S ((S (pfrep_position_step_alignment_pad_left0first)) * u0c) + (pfrep_left_step_alignment_pad_left0)))))) \/ (((exists pfrep_gap_step_alignment_pad_left0firstoutside. pfrep_gap_step_alignment_pad_left0firstoutside+(S N0)=(pfrep_power_step_alignment_pad_left0)) /\ (((pfrep_left_step_alignment_pad_left0)=0))))) -> ((exists pfrep_position_step_alignment_pad_left0second. ((pfrep_position_step_alignment_pad_left0second+S (pfrep_power_step_alignment_pad_left0)=(L+S N0)) /\ ((((exists ff_h_pfp_step_alignment_pad_left0secondentry. ff_h_pfp_step_alignment_pad_left0secondentry + S (pfrep_right_step_alignment_pad_left0) = S ((S (pfrep_position_step_alignment_pad_left0second)) * UP0c)) /\ exists ff_q_pfp_step_alignment_pad_left0secondentry. UP0b = ff_q_pfp_step_alignment_pad_left0secondentry * S ((S (pfrep_position_step_alignment_pad_left0second)) * UP0c) + (pfrep_right_step_alignment_pad_left0)))))) \/ (((exists pfrep_gap_step_alignment_pad_left0secondoutside. pfrep_gap_step_alignment_pad_left0secondoutside+(L+S N0)=(pfrep_power_step_alignment_pad_left0)) /\ (((pfrep_right_step_alignment_pad_left0)=0))))) -> pfrep_left_step_alignment_pad_left0=pfrep_right_step_alignment_pad_left0
  81. 0081specialize prime_field_polynomial_left_pad_equivalent (u0b)
  82. 0082specialize prime_field_polynomial_left_pad_equivalent (u0c)
  83. 0083specialize prime_field_polynomial_left_pad_equivalent (S N0)
  84. 0084specialize prime_field_polynomial_left_pad_equivalent (L)
  85. 0085specialize prime_field_polynomial_left_pad_equivalent (UP0b)
  86. 0086specialize prime_field_polynomial_left_pad_equivalent (UP0c)
  87. 0087apply prime_field_polynomial_left_pad_equivalent
  88. 0088exact hUP0
  89. 0089have hpad_left1 : forall pfrep_power_step_alignment_pad_left1 pfrep_left_step_alignment_pad_left1 pfrep_right_step_alignment_pad_left1. ((exists pfrep_position_step_alignment_pad_left1first. ((pfrep_position_step_alignment_pad_left1first+S (pfrep_power_step_alignment_pad_left1)=(S N1)) /\ ((((exists ff_h_pfp_step_alignment_pad_left1firstentry. ff_h_pfp_step_alignment_pad_left1firstentry + S (pfrep_left_step_alignment_pad_left1) = S ((S (pfrep_position_step_alignment_pad_left1first)) * u1c)) /\ exists ff_q_pfp_step_alignment_pad_left1firstentry. u1b = ff_q_pfp_step_alignment_pad_left1firstentry * S ((S (pfrep_position_step_alignment_pad_left1first)) * u1c) + (pfrep_left_step_alignment_pad_left1)))))) \/ (((exists pfrep_gap_step_alignment_pad_left1firstoutside. pfrep_gap_step_alignment_pad_left1firstoutside+(S N1)=(pfrep_power_step_alignment_pad_left1)) /\ (((pfrep_left_step_alignment_pad_left1)=0))))) -> ((exists pfrep_position_step_alignment_pad_left1second. ((pfrep_position_step_alignment_pad_left1second+S (pfrep_power_step_alignment_pad_left1)=(L+S N1)) /\ ((((exists ff_h_pfp_step_alignment_pad_left1secondentry. ff_h_pfp_step_alignment_pad_left1secondentry + S (pfrep_right_step_alignment_pad_left1) = S ((S (pfrep_position_step_alignment_pad_left1second)) * UP1c)) /\ exists ff_q_pfp_step_alignment_pad_left1secondentry. UP1b = ff_q_pfp_step_alignment_pad_left1secondentry * S ((S (pfrep_position_step_alignment_pad_left1second)) * UP1c) + (pfrep_right_step_alignment_pad_left1)))))) \/ (((exists pfrep_gap_step_alignment_pad_left1secondoutside. pfrep_gap_step_alignment_pad_left1secondoutside+(L+S N1)=(pfrep_power_step_alignment_pad_left1)) /\ (((pfrep_right_step_alignment_pad_left1)=0))))) -> pfrep_left_step_alignment_pad_left1=pfrep_right_step_alignment_pad_left1
  90. 0090specialize prime_field_polynomial_left_pad_equivalent (u1b)
  91. 0091specialize prime_field_polynomial_left_pad_equivalent (u1c)
  92. 0092specialize prime_field_polynomial_left_pad_equivalent (S N1)
  93. 0093specialize prime_field_polynomial_left_pad_equivalent (L)
  94. 0094specialize prime_field_polynomial_left_pad_equivalent (UP1b)
  95. 0095specialize prime_field_polynomial_left_pad_equivalent (UP1c)
  96. 0096apply prime_field_polynomial_left_pad_equivalent
  97. 0097exact hUP1
  98. 0098have hpad_right0 : forall pfrep_power_step_alignment_pad_right0 pfrep_left_step_alignment_pad_right0 pfrep_right_step_alignment_pad_right0. ((exists pfrep_position_step_alignment_pad_right0first. ((pfrep_position_step_alignment_pad_right0first+S (pfrep_power_step_alignment_pad_right0)=(L)) /\ ((((exists ff_h_pfp_step_alignment_pad_right0firstentry. ff_h_pfp_step_alignment_pad_right0firstentry + S (pfrep_left_step_alignment_pad_right0) = S ((S (pfrep_position_step_alignment_pad_right0first)) * v0c)) /\ exists ff_q_pfp_step_alignment_pad_right0firstentry. v0b = ff_q_pfp_step_alignment_pad_right0firstentry * S ((S (pfrep_position_step_alignment_pad_right0first)) * v0c) + (pfrep_left_step_alignment_pad_right0)))))) \/ (((exists pfrep_gap_step_alignment_pad_right0firstoutside. pfrep_gap_step_alignment_pad_right0firstoutside+(L)=(pfrep_power_step_alignment_pad_right0)) /\ (((pfrep_left_step_alignment_pad_right0)=0))))) -> ((exists pfrep_position_step_alignment_pad_right0second. ((pfrep_position_step_alignment_pad_right0second+S (pfrep_power_step_alignment_pad_right0)=(S N0+L)) /\ ((((exists ff_h_pfp_step_alignment_pad_right0secondentry. ff_h_pfp_step_alignment_pad_right0secondentry + S (pfrep_right_step_alignment_pad_right0) = S ((S (pfrep_position_step_alignment_pad_right0second)) * VP0c)) /\ exists ff_q_pfp_step_alignment_pad_right0secondentry. VP0b = ff_q_pfp_step_alignment_pad_right0secondentry * S ((S (pfrep_position_step_alignment_pad_right0second)) * VP0c) + (pfrep_right_step_alignment_pad_right0)))))) \/ (((exists pfrep_gap_step_alignment_pad_right0secondoutside. pfrep_gap_step_alignment_pad_right0secondoutside+(S N0+L)=(pfrep_power_step_alignment_pad_right0)) /\ (((pfrep_right_step_alignment_pad_right0)=0))))) -> pfrep_left_step_alignment_pad_right0=pfrep_right_step_alignment_pad_right0
  99. 0099specialize prime_field_polynomial_left_pad_equivalent (v0b)
  100. 0100specialize prime_field_polynomial_left_pad_equivalent (v0c)
  101. 0101specialize prime_field_polynomial_left_pad_equivalent (L)
  102. 0102specialize prime_field_polynomial_left_pad_equivalent (S N0)
  103. 0103specialize prime_field_polynomial_left_pad_equivalent (VP0b)
  104. 0104specialize prime_field_polynomial_left_pad_equivalent (VP0c)
  105. 0105apply prime_field_polynomial_left_pad_equivalent
  106. 0106exact hVP0
  107. 0107have hcomm_right0 : S N0+L=L+S N0
  108. 0108specialize add_comm (S N0)
  109. 0109specialize add_comm (L)
  110. 0110apply add_comm
  111. 0111rewrite hcomm_right0 at hpad_right0
  112. 0112rewrite hcomm_right0 at hpad_right0
  113. 0113have hpad_right1 : forall pfrep_power_step_alignment_pad_right1 pfrep_left_step_alignment_pad_right1 pfrep_right_step_alignment_pad_right1. ((exists pfrep_position_step_alignment_pad_right1first. ((pfrep_position_step_alignment_pad_right1first+S (pfrep_power_step_alignment_pad_right1)=(L)) /\ ((((exists ff_h_pfp_step_alignment_pad_right1firstentry. ff_h_pfp_step_alignment_pad_right1firstentry + S (pfrep_left_step_alignment_pad_right1) = S ((S (pfrep_position_step_alignment_pad_right1first)) * v1c)) /\ exists ff_q_pfp_step_alignment_pad_right1firstentry. v1b = ff_q_pfp_step_alignment_pad_right1firstentry * S ((S (pfrep_position_step_alignment_pad_right1first)) * v1c) + (pfrep_left_step_alignment_pad_right1)))))) \/ (((exists pfrep_gap_step_alignment_pad_right1firstoutside. pfrep_gap_step_alignment_pad_right1firstoutside+(L)=(pfrep_power_step_alignment_pad_right1)) /\ (((pfrep_left_step_alignment_pad_right1)=0))))) -> ((exists pfrep_position_step_alignment_pad_right1second. ((pfrep_position_step_alignment_pad_right1second+S (pfrep_power_step_alignment_pad_right1)=(S N1+L)) /\ ((((exists ff_h_pfp_step_alignment_pad_right1secondentry. ff_h_pfp_step_alignment_pad_right1secondentry + S (pfrep_right_step_alignment_pad_right1) = S ((S (pfrep_position_step_alignment_pad_right1second)) * VP1c)) /\ exists ff_q_pfp_step_alignment_pad_right1secondentry. VP1b = ff_q_pfp_step_alignment_pad_right1secondentry * S ((S (pfrep_position_step_alignment_pad_right1second)) * VP1c) + (pfrep_right_step_alignment_pad_right1)))))) \/ (((exists pfrep_gap_step_alignment_pad_right1secondoutside. pfrep_gap_step_alignment_pad_right1secondoutside+(S N1+L)=(pfrep_power_step_alignment_pad_right1)) /\ (((pfrep_right_step_alignment_pad_right1)=0))))) -> pfrep_left_step_alignment_pad_right1=pfrep_right_step_alignment_pad_right1
  114. 0114specialize prime_field_polynomial_left_pad_equivalent (v1b)
  115. 0115specialize prime_field_polynomial_left_pad_equivalent (v1c)
  116. 0116specialize prime_field_polynomial_left_pad_equivalent (L)
  117. 0117specialize prime_field_polynomial_left_pad_equivalent (S N1)
  118. 0118specialize prime_field_polynomial_left_pad_equivalent (VP1b)
  119. 0119specialize prime_field_polynomial_left_pad_equivalent (VP1c)
  120. 0120apply prime_field_polynomial_left_pad_equivalent
  121. 0121exact hVP1
  122. 0122have hcomm_right1 : S N1+L=L+S N1
  123. 0123specialize add_comm (S N1)
  124. 0124specialize add_comm (L)
  125. 0125apply add_comm
  126. 0126rewrite hcomm_right1 at hpad_right1
  127. 0127rewrite hcomm_right1 at hpad_right1
  128. 0128have hmiddle_left : forall pfrep_power_step_alignment_middle_left pfrep_left_step_alignment_middle_left pfrep_right_step_alignment_middle_left. ((exists pfrep_position_step_alignment_middle_leftfirst. ((pfrep_position_step_alignment_middle_leftfirst+S (pfrep_power_step_alignment_middle_left)=(L+S N0)) /\ ((((exists ff_h_pfp_step_alignment_middle_leftfirstentry. ff_h_pfp_step_alignment_middle_leftfirstentry + S (pfrep_left_step_alignment_middle_left) = S ((S (pfrep_position_step_alignment_middle_leftfirst)) * UP0c)) /\ exists ff_q_pfp_step_alignment_middle_leftfirstentry. UP0b = ff_q_pfp_step_alignment_middle_leftfirstentry * S ((S (pfrep_position_step_alignment_middle_leftfirst)) * UP0c) + (pfrep_left_step_alignment_middle_left)))))) \/ (((exists pfrep_gap_step_alignment_middle_leftfirstoutside. pfrep_gap_step_alignment_middle_leftfirstoutside+(L+S N0)=(pfrep_power_step_alignment_middle_left)) /\ (((pfrep_left_step_alignment_middle_left)=0))))) -> ((exists pfrep_position_step_alignment_middle_leftsecond. ((pfrep_position_step_alignment_middle_leftsecond+S (pfrep_power_step_alignment_middle_left)=(S N1)) /\ ((((exists ff_h_pfp_step_alignment_middle_leftsecondentry. ff_h_pfp_step_alignment_middle_leftsecondentry + S (pfrep_right_step_alignment_middle_left) = S ((S (pfrep_position_step_alignment_middle_leftsecond)) * u1c)) /\ exists ff_q_pfp_step_alignment_middle_leftsecondentry. u1b = ff_q_pfp_step_alignment_middle_leftsecondentry * S ((S (pfrep_position_step_alignment_middle_leftsecond)) * u1c) + (pfrep_right_step_alignment_middle_left)))))) \/ (((exists pfrep_gap_step_alignment_middle_leftsecondoutside. pfrep_gap_step_alignment_middle_leftsecondoutside+(S N1)=(pfrep_power_step_alignment_middle_left)) /\ (((pfrep_right_step_alignment_middle_left)=0))))) -> pfrep_left_step_alignment_middle_left=pfrep_right_step_alignment_middle_left
  129. 0129specialize prime_field_polynomial_equivalent_transitive (UP0b)
  130. 0130specialize prime_field_polynomial_equivalent_transitive (UP0c)
  131. 0131specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  132. 0132specialize prime_field_polynomial_equivalent_transitive (u0b)
  133. 0133specialize prime_field_polynomial_equivalent_transitive (u0c)
  134. 0134specialize prime_field_polynomial_equivalent_transitive (S N0)
  135. 0135specialize prime_field_polynomial_equivalent_transitive (u1b)
  136. 0136specialize prime_field_polynomial_equivalent_transitive (u1c)
  137. 0137specialize prime_field_polynomial_equivalent_transitive (S N1)
  138. 0138apply prime_field_polynomial_equivalent_transitive
  139. 0139specialize prime_field_polynomial_equivalent_symmetric (u0b)
  140. 0140specialize prime_field_polynomial_equivalent_symmetric (u0c)
  141. 0141specialize prime_field_polynomial_equivalent_symmetric (S N0)
  142. 0142specialize prime_field_polynomial_equivalent_symmetric (UP0b)
  143. 0143specialize prime_field_polynomial_equivalent_symmetric (UP0c)
  144. 0144specialize prime_field_polynomial_equivalent_symmetric (L+S N0)
  145. 0145apply prime_field_polynomial_equivalent_symmetric
  146. 0146exact hpad_left0
  147. 0147exact hshifted
  148. 0148have hequal_left : forall pfrep_power_step_alignment_result_left pfrep_left_step_alignment_result_left pfrep_right_step_alignment_result_left. ((exists pfrep_position_step_alignment_result_leftfirst. ((pfrep_position_step_alignment_result_leftfirst+S (pfrep_power_step_alignment_result_left)=(L+S N0)) /\ ((((exists ff_h_pfp_step_alignment_result_leftfirstentry. ff_h_pfp_step_alignment_result_leftfirstentry + S (pfrep_left_step_alignment_result_left) = S ((S (pfrep_position_step_alignment_result_leftfirst)) * UP0c)) /\ exists ff_q_pfp_step_alignment_result_leftfirstentry. UP0b = ff_q_pfp_step_alignment_result_leftfirstentry * S ((S (pfrep_position_step_alignment_result_leftfirst)) * UP0c) + (pfrep_left_step_alignment_result_left)))))) \/ (((exists pfrep_gap_step_alignment_result_leftfirstoutside. pfrep_gap_step_alignment_result_leftfirstoutside+(L+S N0)=(pfrep_power_step_alignment_result_left)) /\ (((pfrep_left_step_alignment_result_left)=0))))) -> ((exists pfrep_position_step_alignment_result_leftsecond. ((pfrep_position_step_alignment_result_leftsecond+S (pfrep_power_step_alignment_result_left)=(L+S N1)) /\ ((((exists ff_h_pfp_step_alignment_result_leftsecondentry. ff_h_pfp_step_alignment_result_leftsecondentry + S (pfrep_right_step_alignment_result_left) = S ((S (pfrep_position_step_alignment_result_leftsecond)) * UP1c)) /\ exists ff_q_pfp_step_alignment_result_leftsecondentry. UP1b = ff_q_pfp_step_alignment_result_leftsecondentry * S ((S (pfrep_position_step_alignment_result_leftsecond)) * UP1c) + (pfrep_right_step_alignment_result_left)))))) \/ (((exists pfrep_gap_step_alignment_result_leftsecondoutside. pfrep_gap_step_alignment_result_leftsecondoutside+(L+S N1)=(pfrep_power_step_alignment_result_left)) /\ (((pfrep_right_step_alignment_result_left)=0))))) -> pfrep_left_step_alignment_result_left=pfrep_right_step_alignment_result_left
  149. 0149specialize prime_field_polynomial_equivalent_transitive (UP0b)
  150. 0150specialize prime_field_polynomial_equivalent_transitive (UP0c)
  151. 0151specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  152. 0152specialize prime_field_polynomial_equivalent_transitive (u1b)
  153. 0153specialize prime_field_polynomial_equivalent_transitive (u1c)
  154. 0154specialize prime_field_polynomial_equivalent_transitive (S N1)
  155. 0155specialize prime_field_polynomial_equivalent_transitive (UP1b)
  156. 0156specialize prime_field_polynomial_equivalent_transitive (UP1c)
  157. 0157specialize prime_field_polynomial_equivalent_transitive (L+S N1)
  158. 0158apply prime_field_polynomial_equivalent_transitive
  159. 0159exact hmiddle_left
  160. 0160exact hpad_left1
  161. 0161have hmiddle_right : forall pfrep_power_step_alignment_middle_right pfrep_left_step_alignment_middle_right pfrep_right_step_alignment_middle_right. ((exists pfrep_position_step_alignment_middle_rightfirst. ((pfrep_position_step_alignment_middle_rightfirst+S (pfrep_power_step_alignment_middle_right)=(L+S N0)) /\ ((((exists ff_h_pfp_step_alignment_middle_rightfirstentry. ff_h_pfp_step_alignment_middle_rightfirstentry + S (pfrep_left_step_alignment_middle_right) = S ((S (pfrep_position_step_alignment_middle_rightfirst)) * VP0c)) /\ exists ff_q_pfp_step_alignment_middle_rightfirstentry. VP0b = ff_q_pfp_step_alignment_middle_rightfirstentry * S ((S (pfrep_position_step_alignment_middle_rightfirst)) * VP0c) + (pfrep_left_step_alignment_middle_right)))))) \/ (((exists pfrep_gap_step_alignment_middle_rightfirstoutside. pfrep_gap_step_alignment_middle_rightfirstoutside+(L+S N0)=(pfrep_power_step_alignment_middle_right)) /\ (((pfrep_left_step_alignment_middle_right)=0))))) -> ((exists pfrep_position_step_alignment_middle_rightsecond. ((pfrep_position_step_alignment_middle_rightsecond+S (pfrep_power_step_alignment_middle_right)=(L)) /\ ((((exists ff_h_pfp_step_alignment_middle_rightsecondentry. ff_h_pfp_step_alignment_middle_rightsecondentry + S (pfrep_right_step_alignment_middle_right) = S ((S (pfrep_position_step_alignment_middle_rightsecond)) * v1c)) /\ exists ff_q_pfp_step_alignment_middle_rightsecondentry. v1b = ff_q_pfp_step_alignment_middle_rightsecondentry * S ((S (pfrep_position_step_alignment_middle_rightsecond)) * v1c) + (pfrep_right_step_alignment_middle_right)))))) \/ (((exists pfrep_gap_step_alignment_middle_rightsecondoutside. pfrep_gap_step_alignment_middle_rightsecondoutside+(L)=(pfrep_power_step_alignment_middle_right)) /\ (((pfrep_right_step_alignment_middle_right)=0))))) -> pfrep_left_step_alignment_middle_right=pfrep_right_step_alignment_middle_right
  162. 0162specialize prime_field_polynomial_equivalent_transitive (VP0b)
  163. 0163specialize prime_field_polynomial_equivalent_transitive (VP0c)
  164. 0164specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  165. 0165specialize prime_field_polynomial_equivalent_transitive (v0b)
  166. 0166specialize prime_field_polynomial_equivalent_transitive (v0c)
  167. 0167specialize prime_field_polynomial_equivalent_transitive (L)
  168. 0168specialize prime_field_polynomial_equivalent_transitive (v1b)
  169. 0169specialize prime_field_polynomial_equivalent_transitive (v1c)
  170. 0170specialize prime_field_polynomial_equivalent_transitive (L)
  171. 0171apply prime_field_polynomial_equivalent_transitive
  172. 0172specialize prime_field_polynomial_equivalent_symmetric (v0b)
  173. 0173specialize prime_field_polynomial_equivalent_symmetric (v0c)
  174. 0174specialize prime_field_polynomial_equivalent_symmetric (L)
  175. 0175specialize prime_field_polynomial_equivalent_symmetric (VP0b)
  176. 0176specialize prime_field_polynomial_equivalent_symmetric (VP0c)
  177. 0177specialize prime_field_polynomial_equivalent_symmetric (L+S N0)
  178. 0178apply prime_field_polynomial_equivalent_symmetric
  179. 0179exact hpad_right0
  180. 0180exact hscalar_equal
  181. 0181have hequal_right : forall pfrep_power_step_alignment_result_right pfrep_left_step_alignment_result_right pfrep_right_step_alignment_result_right. ((exists pfrep_position_step_alignment_result_rightfirst. ((pfrep_position_step_alignment_result_rightfirst+S (pfrep_power_step_alignment_result_right)=(L+S N0)) /\ ((((exists ff_h_pfp_step_alignment_result_rightfirstentry. ff_h_pfp_step_alignment_result_rightfirstentry + S (pfrep_left_step_alignment_result_right) = S ((S (pfrep_position_step_alignment_result_rightfirst)) * VP0c)) /\ exists ff_q_pfp_step_alignment_result_rightfirstentry. VP0b = ff_q_pfp_step_alignment_result_rightfirstentry * S ((S (pfrep_position_step_alignment_result_rightfirst)) * VP0c) + (pfrep_left_step_alignment_result_right)))))) \/ (((exists pfrep_gap_step_alignment_result_rightfirstoutside. pfrep_gap_step_alignment_result_rightfirstoutside+(L+S N0)=(pfrep_power_step_alignment_result_right)) /\ (((pfrep_left_step_alignment_result_right)=0))))) -> ((exists pfrep_position_step_alignment_result_rightsecond. ((pfrep_position_step_alignment_result_rightsecond+S (pfrep_power_step_alignment_result_right)=(L+S N1)) /\ ((((exists ff_h_pfp_step_alignment_result_rightsecondentry. ff_h_pfp_step_alignment_result_rightsecondentry + S (pfrep_right_step_alignment_result_right) = S ((S (pfrep_position_step_alignment_result_rightsecond)) * VP1c)) /\ exists ff_q_pfp_step_alignment_result_rightsecondentry. VP1b = ff_q_pfp_step_alignment_result_rightsecondentry * S ((S (pfrep_position_step_alignment_result_rightsecond)) * VP1c) + (pfrep_right_step_alignment_result_right)))))) \/ (((exists pfrep_gap_step_alignment_result_rightsecondoutside. pfrep_gap_step_alignment_result_rightsecondoutside+(L+S N1)=(pfrep_power_step_alignment_result_right)) /\ (((pfrep_right_step_alignment_result_right)=0))))) -> pfrep_left_step_alignment_result_right=pfrep_right_step_alignment_result_right
  182. 0182specialize prime_field_polynomial_equivalent_transitive (VP0b)
  183. 0183specialize prime_field_polynomial_equivalent_transitive (VP0c)
  184. 0184specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  185. 0185specialize prime_field_polynomial_equivalent_transitive (v1b)
  186. 0186specialize prime_field_polynomial_equivalent_transitive (v1c)
  187. 0187specialize prime_field_polynomial_equivalent_transitive (L)
  188. 0188specialize prime_field_polynomial_equivalent_transitive (VP1b)
  189. 0189specialize prime_field_polynomial_equivalent_transitive (VP1c)
  190. 0190specialize prime_field_polynomial_equivalent_transitive (L+S N1)
  191. 0191apply prime_field_polynomial_equivalent_transitive
  192. 0192exact hmiddle_right
  193. 0193exact hpad_right1
  194. 0194specialize prime_field_polynomial_add_equivalent_congruent (p)
  195. 0195specialize prime_field_polynomial_add_equivalent_congruent (UP0b)
  196. 0196specialize prime_field_polynomial_add_equivalent_congruent (UP0c)
  197. 0197specialize prime_field_polynomial_add_equivalent_congruent (VP0b)
  198. 0198specialize prime_field_polynomial_add_equivalent_congruent (VP0c)
  199. 0199specialize prime_field_polynomial_add_equivalent_congruent (z0b)
  200. 0200specialize prime_field_polynomial_add_equivalent_congruent (z0c)
  201. 0201specialize prime_field_polynomial_add_equivalent_congruent (L+S N0)
  202. 0202specialize prime_field_polynomial_add_equivalent_congruent (UP1b)
  203. 0203specialize prime_field_polynomial_add_equivalent_congruent (UP1c)
  204. 0204specialize prime_field_polynomial_add_equivalent_congruent (VP1b)
  205. 0205specialize prime_field_polynomial_add_equivalent_congruent (VP1c)
  206. 0206specialize prime_field_polynomial_add_equivalent_congruent (z1b)
  207. 0207specialize prime_field_polynomial_add_equivalent_congruent (z1c)
  208. 0208specialize prime_field_polynomial_add_equivalent_congruent (L+S N1)
  209. 0209apply prime_field_polynomial_add_equivalent_congruent
  210. 0210exact hp
  211. 0211exact hequal_left
  212. 0212exact hequal_right
  213. 0213exact hZ0
  214. 0214exact hZ1