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.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable
Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.
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)
Complete tactic proof in conservative notation
All 104 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
01Fix variables and assumptionsL1–10
Work with arbitrary variables or the premises of the current implication.