PG0024 — prime_field_polynomial_nested_empty_right_equivalent

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 pb pc N cb cc qb qc K rb rc U sb sc V. (~(p=0)) -> (((forall fom_index_pfp_associativity_empty_Qleft. (exists fom_gap_pfp_associativity_empty_Qleft_index_bound. fom_gap_pfp_associativity_empty_Qleft_index_bound + S (fom_index_pfp_associativity_empty_Qleft) = M) -> exists fom_value_pfp_associativity_empty_Qleft. ((((exists fom_beta_height_pfp_associativity_empty_Qleft_entry. fom_beta_height_pfp_associativity_empty_Qleft_entry + S (fom_value_pfp_associativity_empty_Qleft) = S ((S (fom_index_pfp_associativity_empty_Qleft)) * bc)) /\ exists fom_beta_quotient_pfp_associativity_empty_Qleft_entry. bb = fom_beta_quotient_pfp_associativity_empty_Qleft_entry * S ((S (fom_index_pfp_associativity_empty_Qleft)) * bc) + (fom_value_pfp_associativity_empty_Qleft))) /\ (exists fom_gap_pfp_associativity_empty_Qleft_value_bound. fom_gap_pfp_associativity_empty_Qleft_value_bound + S (fom_value_pfp_associativity_empty_Qleft) = p))) /\ (((forall fom_index_pfp_associativity_empty_Qright. (exists fom_gap_pfp_associativity_empty_Qright_index_bound. fom_gap_pfp_associativity_empty_Qright_index_bound + S (fom_index_pfp_associativity_empty_Qright) = 0) -> exists fom_value_pfp_associativity_empty_Qright. ((((exists fom_beta_height_pfp_associativity_empty_Qright_entry. fom_beta_height_pfp_associativity_empty_Qright_entry + S (fom_value_pfp_associativity_empty_Qright) = S ((S (fom_index_pfp_associativity_empty_Qright)) * cc)) /\ exists fom_beta_quotient_pfp_associativity_empty_Qright_entry. cb = fom_beta_quotient_pfp_associativity_empty_Qright_entry * S ((S (fom_index_pfp_associativity_empty_Qright)) * cc) + (fom_value_pfp_associativity_empty_Qright))) /\ (exists fom_gap_pfp_associativity_empty_Qright_value_bound. fom_gap_pfp_associativity_empty_Qright_value_bound + S (fom_value_pfp_associativity_empty_Qright) = p))) /\ (((((((M)=0 \/ (0)=0) /\ (((K)=0)))) \/ (((~((M)=0)) /\ (((~((0)=0)) /\ (((M)+(0)=S (K)))))))) /\ ((forall pfc_index_associativity_empty_Qcoefficients. (exists pfa_gap_associativity_empty_Qcoefficientsbound. pfa_gap_associativity_empty_Qcoefficientsbound + S (pfc_index_associativity_empty_Qcoefficients) = (K)) -> exists pfc_value_associativity_empty_Qcoefficients. ((((exists ff_h_pfp_associativity_empty_Qcoefficientsentry. ff_h_pfp_associativity_empty_Qcoefficientsentry + S (pfc_value_associativity_empty_Qcoefficients) = S ((S (pfc_index_associativity_empty_Qcoefficients)) * qc)) /\ exists ff_q_pfp_associativity_empty_Qcoefficientsentry. qb = ff_q_pfp_associativity_empty_Qcoefficientsentry * S ((S (pfc_index_associativity_empty_Qcoefficients)) * qc) + (pfc_value_associativity_empty_Qcoefficients))) /\ ((exists pfc_terms_code_associativity_empty_Qcoefficientscoefficient pfc_terms_scale_associativity_empty_Qcoefficientscoefficient pfc_natural_sum_associativity_empty_Qcoefficientscoefficient. ((forall pfc_index_associativity_empty_Qcoefficientscoefficientdiagonal. (exists pfa_gap_associativity_empty_Qcoefficientscoefficientdiagonalbound. pfa_gap_associativity_empty_Qcoefficientscoefficientdiagonalbound + S (pfc_index_associativity_empty_Qcoefficientscoefficientdiagonal) = (S (pfc_index_associativity_empty_Qcoefficients))) -> exists pfc_value_associativity_empty_Qcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associativity_empty_Qcoefficientscoefficientdiagonalentry. ff_h_pfp_associativity_empty_Qcoefficientscoefficientdiagonalentry + S (pfc_value_associativity_empty_Qcoefficientscoefficientdiagonal) = S ((S (pfc_index_associativity_empty_Qcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_empty_Qcoefficientscoefficient)) /\ exists ff_q_pfp_associativity_empty_Qcoefficientscoefficientdiagonalentry. pfc_terms_code_associativity_empty_Qcoefficientscoefficient = ff_q_pfp_associativity_empty_Qcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associativity_empty_Qcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_empty_Qcoefficientscoefficient) + (pfc_value_associativity_empty_Qcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associativity_empty_Qcoefficientscoefficientdiagonalterm pfc_left_associativity_empty_Qcoefficientscoefficientdiagonalterm pfc_right_associativity_empty_Qcoefficientscoefficientdiagonalterm. (((pfc_index_associativity_empty_Qcoefficientscoefficientdiagonal)+pfc_complement_associativity_empty_Qcoefficientscoefficientdiagonalterm=(pfc_index_associativity_empty_Qcoefficients)) /\ ((((((exists pfa_gap_associativity_empty_Qcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associativity_empty_Qcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associativity_empty_Qcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_associativity_empty_Qcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associativity_empty_Qcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associativity_empty_Qcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associativity_empty_Qcoefficientscoefficientdiagonal)) * bc)) /\ exists ff_q_pfp_associativity_empty_Qcoefficientscoefficientdiagonaltermleftentry. bb = ff_q_pfp_associativity_empty_Qcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associativity_empty_Qcoefficientscoefficientdiagonal)) * bc) + (pfc_left_associativity_empty_Qcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_empty_Qcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associativity_empty_Qcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_associativity_empty_Qcoefficientscoefficientdiagonal)) /\ (((pfc_left_associativity_empty_Qcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associativity_empty_Qcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associativity_empty_Qcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associativity_empty_Qcoefficientscoefficientdiagonalterm) = (0)) /\ ((((exists ff_h_pfp_associativity_empty_Qcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associativity_empty_Qcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associativity_empty_Qcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associativity_empty_Qcoefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_associativity_empty_Qcoefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_associativity_empty_Qcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associativity_empty_Qcoefficientscoefficientdiagonalterm)) * cc) + (pfc_right_associativity_empty_Qcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_empty_Qcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associativity_empty_Qcoefficientscoefficientdiagonaltermrightoutside+(0)=(pfc_complement_associativity_empty_Qcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associativity_empty_Qcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associativity_empty_Qcoefficientscoefficientdiagonal)=pfc_left_associativity_empty_Qcoefficientscoefficientdiagonalterm*pfc_right_associativity_empty_Qcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associativity_empty_Qcoefficientscoefficientsum fs_v_pfc_associativity_empty_Qcoefficientscoefficientsum. ((((exists fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_start. fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associativity_empty_Qcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_start. fs_u_pfc_associativity_empty_Qcoefficientscoefficientsum = fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associativity_empty_Qcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_terminal. fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associativity_empty_Qcoefficientscoefficient) = S ((S (S (pfc_index_associativity_empty_Qcoefficients))) * fs_v_pfc_associativity_empty_Qcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_terminal. fs_u_pfc_associativity_empty_Qcoefficientscoefficientsum = fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associativity_empty_Qcoefficients))) * fs_v_pfc_associativity_empty_Qcoefficientscoefficientsum) + (pfc_natural_sum_associativity_empty_Qcoefficientscoefficient))) /\ forall fs_i_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps = S (pfc_index_associativity_empty_Qcoefficients)) -> exists fs_a_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps fs_r_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps fs_s_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_empty_Qcoefficientscoefficient)) /\ exists fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associativity_empty_Qcoefficientscoefficient = fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_empty_Qcoefficientscoefficient) + (fs_a_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Qcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associativity_empty_Qcoefficientscoefficientsum = fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Qcoefficientscoefficientsum) + (fs_r_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Qcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associativity_empty_Qcoefficientscoefficientsum = fs_q_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Qcoefficientscoefficientsum) + (fs_s_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps = fs_r_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps + fs_a_pfc_associativity_empty_Qcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associativity_empty_Qcoefficientscoefficientresiduebound. pfa_gap_associativity_empty_Qcoefficientscoefficientresiduebound + S (pfc_value_associativity_empty_Qcoefficients) = (p)) /\ ((exists pfa_offset_left_associativity_empty_Qcoefficientscoefficientresiduecongruence pfa_offset_right_associativity_empty_Qcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associativity_empty_Qcoefficientscoefficient) + (p) * pfa_offset_left_associativity_empty_Qcoefficientscoefficientresiduecongruence = (pfc_value_associativity_empty_Qcoefficients) + (p) * pfa_offset_right_associativity_empty_Qcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_associativity_empty_Rleft. (exists fom_gap_pfp_associativity_empty_Rleft_index_bound. fom_gap_pfp_associativity_empty_Rleft_index_bound + S (fom_index_pfp_associativity_empty_Rleft) = N) -> exists fom_value_pfp_associativity_empty_Rleft. ((((exists fom_beta_height_pfp_associativity_empty_Rleft_entry. fom_beta_height_pfp_associativity_empty_Rleft_entry + S (fom_value_pfp_associativity_empty_Rleft) = S ((S (fom_index_pfp_associativity_empty_Rleft)) * pc)) /\ exists fom_beta_quotient_pfp_associativity_empty_Rleft_entry. pb = fom_beta_quotient_pfp_associativity_empty_Rleft_entry * S ((S (fom_index_pfp_associativity_empty_Rleft)) * pc) + (fom_value_pfp_associativity_empty_Rleft))) /\ (exists fom_gap_pfp_associativity_empty_Rleft_value_bound. fom_gap_pfp_associativity_empty_Rleft_value_bound + S (fom_value_pfp_associativity_empty_Rleft) = p))) /\ (((forall fom_index_pfp_associativity_empty_Rright. (exists fom_gap_pfp_associativity_empty_Rright_index_bound. fom_gap_pfp_associativity_empty_Rright_index_bound + S (fom_index_pfp_associativity_empty_Rright) = 0) -> exists fom_value_pfp_associativity_empty_Rright. ((((exists fom_beta_height_pfp_associativity_empty_Rright_entry. fom_beta_height_pfp_associativity_empty_Rright_entry + S (fom_value_pfp_associativity_empty_Rright) = S ((S (fom_index_pfp_associativity_empty_Rright)) * cc)) /\ exists fom_beta_quotient_pfp_associativity_empty_Rright_entry. cb = fom_beta_quotient_pfp_associativity_empty_Rright_entry * S ((S (fom_index_pfp_associativity_empty_Rright)) * cc) + (fom_value_pfp_associativity_empty_Rright))) /\ (exists fom_gap_pfp_associativity_empty_Rright_value_bound. fom_gap_pfp_associativity_empty_Rright_value_bound + S (fom_value_pfp_associativity_empty_Rright) = p))) /\ (((((((N)=0 \/ (0)=0) /\ (((U)=0)))) \/ (((~((N)=0)) /\ (((~((0)=0)) /\ (((N)+(0)=S (U)))))))) /\ ((forall pfc_index_associativity_empty_Rcoefficients. (exists pfa_gap_associativity_empty_Rcoefficientsbound. pfa_gap_associativity_empty_Rcoefficientsbound + S (pfc_index_associativity_empty_Rcoefficients) = (U)) -> exists pfc_value_associativity_empty_Rcoefficients. ((((exists ff_h_pfp_associativity_empty_Rcoefficientsentry. ff_h_pfp_associativity_empty_Rcoefficientsentry + S (pfc_value_associativity_empty_Rcoefficients) = S ((S (pfc_index_associativity_empty_Rcoefficients)) * rc)) /\ exists ff_q_pfp_associativity_empty_Rcoefficientsentry. rb = ff_q_pfp_associativity_empty_Rcoefficientsentry * S ((S (pfc_index_associativity_empty_Rcoefficients)) * rc) + (pfc_value_associativity_empty_Rcoefficients))) /\ ((exists pfc_terms_code_associativity_empty_Rcoefficientscoefficient pfc_terms_scale_associativity_empty_Rcoefficientscoefficient pfc_natural_sum_associativity_empty_Rcoefficientscoefficient. ((forall pfc_index_associativity_empty_Rcoefficientscoefficientdiagonal. (exists pfa_gap_associativity_empty_Rcoefficientscoefficientdiagonalbound. pfa_gap_associativity_empty_Rcoefficientscoefficientdiagonalbound + S (pfc_index_associativity_empty_Rcoefficientscoefficientdiagonal) = (S (pfc_index_associativity_empty_Rcoefficients))) -> exists pfc_value_associativity_empty_Rcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associativity_empty_Rcoefficientscoefficientdiagonalentry. ff_h_pfp_associativity_empty_Rcoefficientscoefficientdiagonalentry + S (pfc_value_associativity_empty_Rcoefficientscoefficientdiagonal) = S ((S (pfc_index_associativity_empty_Rcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_empty_Rcoefficientscoefficient)) /\ exists ff_q_pfp_associativity_empty_Rcoefficientscoefficientdiagonalentry. pfc_terms_code_associativity_empty_Rcoefficientscoefficient = ff_q_pfp_associativity_empty_Rcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associativity_empty_Rcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_empty_Rcoefficientscoefficient) + (pfc_value_associativity_empty_Rcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associativity_empty_Rcoefficientscoefficientdiagonalterm pfc_left_associativity_empty_Rcoefficientscoefficientdiagonalterm pfc_right_associativity_empty_Rcoefficientscoefficientdiagonalterm. (((pfc_index_associativity_empty_Rcoefficientscoefficientdiagonal)+pfc_complement_associativity_empty_Rcoefficientscoefficientdiagonalterm=(pfc_index_associativity_empty_Rcoefficients)) /\ ((((((exists pfa_gap_associativity_empty_Rcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associativity_empty_Rcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associativity_empty_Rcoefficientscoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_associativity_empty_Rcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associativity_empty_Rcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associativity_empty_Rcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associativity_empty_Rcoefficientscoefficientdiagonal)) * pc)) /\ exists ff_q_pfp_associativity_empty_Rcoefficientscoefficientdiagonaltermleftentry. pb = ff_q_pfp_associativity_empty_Rcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associativity_empty_Rcoefficientscoefficientdiagonal)) * pc) + (pfc_left_associativity_empty_Rcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_empty_Rcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associativity_empty_Rcoefficientscoefficientdiagonaltermleftoutside+(N)=(pfc_index_associativity_empty_Rcoefficientscoefficientdiagonal)) /\ (((pfc_left_associativity_empty_Rcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associativity_empty_Rcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associativity_empty_Rcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associativity_empty_Rcoefficientscoefficientdiagonalterm) = (0)) /\ ((((exists ff_h_pfp_associativity_empty_Rcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associativity_empty_Rcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associativity_empty_Rcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associativity_empty_Rcoefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_associativity_empty_Rcoefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_associativity_empty_Rcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associativity_empty_Rcoefficientscoefficientdiagonalterm)) * cc) + (pfc_right_associativity_empty_Rcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_empty_Rcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associativity_empty_Rcoefficientscoefficientdiagonaltermrightoutside+(0)=(pfc_complement_associativity_empty_Rcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associativity_empty_Rcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associativity_empty_Rcoefficientscoefficientdiagonal)=pfc_left_associativity_empty_Rcoefficientscoefficientdiagonalterm*pfc_right_associativity_empty_Rcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associativity_empty_Rcoefficientscoefficientsum fs_v_pfc_associativity_empty_Rcoefficientscoefficientsum. ((((exists fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_start. fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associativity_empty_Rcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_start. fs_u_pfc_associativity_empty_Rcoefficientscoefficientsum = fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associativity_empty_Rcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_terminal. fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associativity_empty_Rcoefficientscoefficient) = S ((S (S (pfc_index_associativity_empty_Rcoefficients))) * fs_v_pfc_associativity_empty_Rcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_terminal. fs_u_pfc_associativity_empty_Rcoefficientscoefficientsum = fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associativity_empty_Rcoefficients))) * fs_v_pfc_associativity_empty_Rcoefficientscoefficientsum) + (pfc_natural_sum_associativity_empty_Rcoefficientscoefficient))) /\ forall fs_i_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps = S (pfc_index_associativity_empty_Rcoefficients)) -> exists fs_a_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps fs_r_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps fs_s_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_empty_Rcoefficientscoefficient)) /\ exists fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associativity_empty_Rcoefficientscoefficient = fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_empty_Rcoefficientscoefficient) + (fs_a_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Rcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associativity_empty_Rcoefficientscoefficientsum = fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Rcoefficientscoefficientsum) + (fs_r_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Rcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associativity_empty_Rcoefficientscoefficientsum = fs_q_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Rcoefficientscoefficientsum) + (fs_s_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps = fs_r_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps + fs_a_pfc_associativity_empty_Rcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associativity_empty_Rcoefficientscoefficientresiduebound. pfa_gap_associativity_empty_Rcoefficientscoefficientresiduebound + S (pfc_value_associativity_empty_Rcoefficients) = (p)) /\ ((exists pfa_offset_left_associativity_empty_Rcoefficientscoefficientresiduecongruence pfa_offset_right_associativity_empty_Rcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associativity_empty_Rcoefficientscoefficient) + (p) * pfa_offset_left_associativity_empty_Rcoefficientscoefficientresiduecongruence = (pfc_value_associativity_empty_Rcoefficients) + (p) * pfa_offset_right_associativity_empty_Rcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_associativity_empty_Sleft. (exists fom_gap_pfp_associativity_empty_Sleft_index_bound. fom_gap_pfp_associativity_empty_Sleft_index_bound + S (fom_index_pfp_associativity_empty_Sleft) = L) -> exists fom_value_pfp_associativity_empty_Sleft. ((((exists fom_beta_height_pfp_associativity_empty_Sleft_entry. fom_beta_height_pfp_associativity_empty_Sleft_entry + S (fom_value_pfp_associativity_empty_Sleft) = S ((S (fom_index_pfp_associativity_empty_Sleft)) * ac)) /\ exists fom_beta_quotient_pfp_associativity_empty_Sleft_entry. ab = fom_beta_quotient_pfp_associativity_empty_Sleft_entry * S ((S (fom_index_pfp_associativity_empty_Sleft)) * ac) + (fom_value_pfp_associativity_empty_Sleft))) /\ (exists fom_gap_pfp_associativity_empty_Sleft_value_bound. fom_gap_pfp_associativity_empty_Sleft_value_bound + S (fom_value_pfp_associativity_empty_Sleft) = p))) /\ (((forall fom_index_pfp_associativity_empty_Sright. (exists fom_gap_pfp_associativity_empty_Sright_index_bound. fom_gap_pfp_associativity_empty_Sright_index_bound + S (fom_index_pfp_associativity_empty_Sright) = K) -> exists fom_value_pfp_associativity_empty_Sright. ((((exists fom_beta_height_pfp_associativity_empty_Sright_entry. fom_beta_height_pfp_associativity_empty_Sright_entry + S (fom_value_pfp_associativity_empty_Sright) = S ((S (fom_index_pfp_associativity_empty_Sright)) * qc)) /\ exists fom_beta_quotient_pfp_associativity_empty_Sright_entry. qb = fom_beta_quotient_pfp_associativity_empty_Sright_entry * S ((S (fom_index_pfp_associativity_empty_Sright)) * qc) + (fom_value_pfp_associativity_empty_Sright))) /\ (exists fom_gap_pfp_associativity_empty_Sright_value_bound. fom_gap_pfp_associativity_empty_Sright_value_bound + S (fom_value_pfp_associativity_empty_Sright) = p))) /\ (((((((L)=0 \/ (K)=0) /\ (((V)=0)))) \/ (((~((L)=0)) /\ (((~((K)=0)) /\ (((L)+(K)=S (V)))))))) /\ ((forall pfc_index_associativity_empty_Scoefficients. (exists pfa_gap_associativity_empty_Scoefficientsbound. pfa_gap_associativity_empty_Scoefficientsbound + S (pfc_index_associativity_empty_Scoefficients) = (V)) -> exists pfc_value_associativity_empty_Scoefficients. ((((exists ff_h_pfp_associativity_empty_Scoefficientsentry. ff_h_pfp_associativity_empty_Scoefficientsentry + S (pfc_value_associativity_empty_Scoefficients) = S ((S (pfc_index_associativity_empty_Scoefficients)) * sc)) /\ exists ff_q_pfp_associativity_empty_Scoefficientsentry. sb = ff_q_pfp_associativity_empty_Scoefficientsentry * S ((S (pfc_index_associativity_empty_Scoefficients)) * sc) + (pfc_value_associativity_empty_Scoefficients))) /\ ((exists pfc_terms_code_associativity_empty_Scoefficientscoefficient pfc_terms_scale_associativity_empty_Scoefficientscoefficient pfc_natural_sum_associativity_empty_Scoefficientscoefficient. ((forall pfc_index_associativity_empty_Scoefficientscoefficientdiagonal. (exists pfa_gap_associativity_empty_Scoefficientscoefficientdiagonalbound. pfa_gap_associativity_empty_Scoefficientscoefficientdiagonalbound + S (pfc_index_associativity_empty_Scoefficientscoefficientdiagonal) = (S (pfc_index_associativity_empty_Scoefficients))) -> exists pfc_value_associativity_empty_Scoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associativity_empty_Scoefficientscoefficientdiagonalentry. ff_h_pfp_associativity_empty_Scoefficientscoefficientdiagonalentry + S (pfc_value_associativity_empty_Scoefficientscoefficientdiagonal) = S ((S (pfc_index_associativity_empty_Scoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_empty_Scoefficientscoefficient)) /\ exists ff_q_pfp_associativity_empty_Scoefficientscoefficientdiagonalentry. pfc_terms_code_associativity_empty_Scoefficientscoefficient = ff_q_pfp_associativity_empty_Scoefficientscoefficientdiagonalentry * S ((S (pfc_index_associativity_empty_Scoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_empty_Scoefficientscoefficient) + (pfc_value_associativity_empty_Scoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associativity_empty_Scoefficientscoefficientdiagonalterm pfc_left_associativity_empty_Scoefficientscoefficientdiagonalterm pfc_right_associativity_empty_Scoefficientscoefficientdiagonalterm. (((pfc_index_associativity_empty_Scoefficientscoefficientdiagonal)+pfc_complement_associativity_empty_Scoefficientscoefficientdiagonalterm=(pfc_index_associativity_empty_Scoefficients)) /\ ((((((exists pfa_gap_associativity_empty_Scoefficientscoefficientdiagonaltermleftinside. pfa_gap_associativity_empty_Scoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associativity_empty_Scoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_associativity_empty_Scoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associativity_empty_Scoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associativity_empty_Scoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associativity_empty_Scoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_associativity_empty_Scoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_associativity_empty_Scoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associativity_empty_Scoefficientscoefficientdiagonal)) * ac) + (pfc_left_associativity_empty_Scoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_empty_Scoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associativity_empty_Scoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_associativity_empty_Scoefficientscoefficientdiagonal)) /\ (((pfc_left_associativity_empty_Scoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associativity_empty_Scoefficientscoefficientdiagonaltermrightinside. pfa_gap_associativity_empty_Scoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associativity_empty_Scoefficientscoefficientdiagonalterm) = (K)) /\ ((((exists ff_h_pfp_associativity_empty_Scoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associativity_empty_Scoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associativity_empty_Scoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associativity_empty_Scoefficientscoefficientdiagonalterm)) * qc)) /\ exists ff_q_pfp_associativity_empty_Scoefficientscoefficientdiagonaltermrightentry. qb = ff_q_pfp_associativity_empty_Scoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associativity_empty_Scoefficientscoefficientdiagonalterm)) * qc) + (pfc_right_associativity_empty_Scoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_empty_Scoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associativity_empty_Scoefficientscoefficientdiagonaltermrightoutside+(K)=(pfc_complement_associativity_empty_Scoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associativity_empty_Scoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associativity_empty_Scoefficientscoefficientdiagonal)=pfc_left_associativity_empty_Scoefficientscoefficientdiagonalterm*pfc_right_associativity_empty_Scoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associativity_empty_Scoefficientscoefficientsum fs_v_pfc_associativity_empty_Scoefficientscoefficientsum. ((((exists fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_start. fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associativity_empty_Scoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_start. fs_u_pfc_associativity_empty_Scoefficientscoefficientsum = fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associativity_empty_Scoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_terminal. fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associativity_empty_Scoefficientscoefficient) = S ((S (S (pfc_index_associativity_empty_Scoefficients))) * fs_v_pfc_associativity_empty_Scoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_terminal. fs_u_pfc_associativity_empty_Scoefficientscoefficientsum = fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associativity_empty_Scoefficients))) * fs_v_pfc_associativity_empty_Scoefficientscoefficientsum) + (pfc_natural_sum_associativity_empty_Scoefficientscoefficient))) /\ forall fs_i_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps = S (pfc_index_associativity_empty_Scoefficients)) -> exists fs_a_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps fs_r_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps fs_s_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_empty_Scoefficientscoefficient)) /\ exists fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associativity_empty_Scoefficientscoefficient = fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_empty_Scoefficientscoefficient) + (fs_a_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Scoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associativity_empty_Scoefficientscoefficientsum = fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Scoefficientscoefficientsum) + (fs_r_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Scoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associativity_empty_Scoefficientscoefficientsum = fs_q_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_empty_Scoefficientscoefficientsum) + (fs_s_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps = fs_r_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps + fs_a_pfc_associativity_empty_Scoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associativity_empty_Scoefficientscoefficientresiduebound. pfa_gap_associativity_empty_Scoefficientscoefficientresiduebound + S (pfc_value_associativity_empty_Scoefficients) = (p)) /\ ((exists pfa_offset_left_associativity_empty_Scoefficientscoefficientresiduecongruence pfa_offset_right_associativity_empty_Scoefficientscoefficientresiduecongruence. (pfc_natural_sum_associativity_empty_Scoefficientscoefficient) + (p) * pfa_offset_left_associativity_empty_Scoefficientscoefficientresiduecongruence = (pfc_value_associativity_empty_Scoefficients) + (p) * pfa_offset_right_associativity_empty_Scoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_associativity_empty_result pfrep_left_associativity_empty_result pfrep_right_associativity_empty_result. ((exists pfrep_position_associativity_empty_resultfirst. ((pfrep_position_associativity_empty_resultfirst+S (pfrep_power_associativity_empty_result)=(U)) /\ ((((exists ff_h_pfp_associativity_empty_resultfirstentry. ff_h_pfp_associativity_empty_resultfirstentry + S (pfrep_left_associativity_empty_result) = S ((S (pfrep_position_associativity_empty_resultfirst)) * rc)) /\ exists ff_q_pfp_associativity_empty_resultfirstentry. rb = ff_q_pfp_associativity_empty_resultfirstentry * S ((S (pfrep_position_associativity_empty_resultfirst)) * rc) + (pfrep_left_associativity_empty_result)))))) \/ (((exists pfrep_gap_associativity_empty_resultfirstoutside. pfrep_gap_associativity_empty_resultfirstoutside+(U)=(pfrep_power_associativity_empty_result)) /\ (((pfrep_left_associativity_empty_result)=0))))) -> ((exists pfrep_position_associativity_empty_resultsecond. ((pfrep_position_associativity_empty_resultsecond+S (pfrep_power_associativity_empty_result)=(V)) /\ ((((exists ff_h_pfp_associativity_empty_resultsecondentry. ff_h_pfp_associativity_empty_resultsecondentry + S (pfrep_right_associativity_empty_result) = S ((S (pfrep_position_associativity_empty_resultsecond)) * sc)) /\ exists ff_q_pfp_associativity_empty_resultsecondentry. sb = ff_q_pfp_associativity_empty_resultsecondentry * S ((S (pfrep_position_associativity_empty_resultsecond)) * sc) + (pfrep_right_associativity_empty_result)))))) \/ (((exists pfrep_gap_associativity_empty_resultsecondoutside. pfrep_gap_associativity_empty_resultsecondoutside+(V)=(pfrep_power_associativity_empty_result)) /\ (((pfrep_right_associativity_empty_result)=0))))) -> pfrep_left_associativity_empty_result=pfrep_right_associativity_empty_result)

Constructive proof overview

Generated structural guide

At every nonzero modulus, actual Q=B*empty, R=P*empty and S=A*Q have formally equivalent all-zero outputs, for arbitrary actual P. The argument constructs the genuine empty zero-prefix fact and transports it through the real products; it assumes neither P=AB nor an output-length shortcut.

The unchanged tactic script uses 5 declared prerequisites and contains 104 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_repeat_empty Alpha theorem; checked-use authorized prime_field_polynomial_convolution_zero_right Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_transitive Alpha theorem; checked-use authorized prime_field_polynomial_zero_prefix_equivalent_empty Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_symmetric Alpha theorem; checked-use authorized

Direct dependents

PG0025 prime_field_polynomial_convolution_associative_equivalent

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

104 script commands · 13 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.

01Fix variables and assumptionsL1–10

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

L1
intro p
L2
intro ab
L3
intro ac
L4
intro L
L5
intro bb
L6
intro bc
L7
intro M
L8
intro pb
L9
intro pc
L10
intro N

02Fix variables and assumptionsL11–20

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

L11
intro cb
L12
intro cc
L13
intro qb
L14
intro qc
L15
intro K
L16
intro rb
L17
intro rc
L18
intro U
L19
intro sb
L20
intro sc

03Fix variables and assumptionsL21–25

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

L21
intro V
L22
intro hp
L23
intro hQ
L24
intro hR
L25
intro hS

04Establish hemptyL26–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta repeat empty.

L26
have hempty : forall pfp_repeat_index_associativity_empty_prefix. (exists pfa_gap_associativity_empty_prefixindex. pfa_gap_associativity_empty_prefixindex + S (pfp_repeat_index_associativity_empty_prefix) = (0)) -> (((exists ff_h_pfp_associativity_empty_prefixentry. ff_h_pfp_associativity_empty_prefixentry + S (0) = S ((S (pfp_repeat_index_associativity_empty_prefix)) * cc)) /\ exists ff_q_pfp_associativity_empty_prefixentry. cb = ff_q_pfp_associativity_empty_prefixentry * S ((S (pfp_repeat_index_associativity_empty_prefix)) * cc) + (0)))
L27
specialize beta_repeat_empty (cb)
L28
specialize beta_repeat_empty (cc)
L29
specialize beta_repeat_empty (0)
L30
specialize beta_repeat_empty (0)
L31
apply beta_repeat_empty
L32
refl

05Establish hQzeroL33–42

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

L33
have hQzero : forall pfp_repeat_index_associativity_hQzero. (exists pfa_gap_associativity_hQzeroindex. pfa_gap_associativity_hQzeroindex + S (pfp_repeat_index_associativity_hQzero) = (K)) -> (((exists ff_h_pfp_associativity_hQzeroentry. ff_h_pfp_associativity_hQzeroentry + S (0) = S ((S (pfp_repeat_index_associativity_hQzero)) * qc)) /\ exists ff_q_pfp_associativity_hQzeroentry. qb = ff_q_pfp_associativity_hQzeroentry * S ((S (pfp_repeat_index_associativity_hQzero)) * qc) + (0)))
L34
specialize prime_field_polynomial_convolution_zero_right (p)
L35
specialize prime_field_polynomial_convolution_zero_right (bb)
L36
specialize prime_field_polynomial_convolution_zero_right (bc)
L37
specialize prime_field_polynomial_convolution_zero_right (M)
L38
specialize prime_field_polynomial_convolution_zero_right (cb)
L39
specialize prime_field_polynomial_convolution_zero_right (cc)
L40
specialize prime_field_polynomial_convolution_zero_right (0)
L41
specialize prime_field_polynomial_convolution_zero_right (qb)
L42
specialize prime_field_polynomial_convolution_zero_right (qc)

06Use earlier factsL43–47