Draft universal rightmost-length induction for formal equivalence of actual (A*B)*C and A*(B*C). The induction predicate quantifies all rightmost codes and proper-length output triples, the successor genuinely constructs three prefix products and decodes the actual endpoint, and the empty base retains arbitrary encodings. This statement is not a successful proof observation until its original body and its exact step dependency are genuinely checked.
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 J qb qc K rb rc U sb sc V. (~((p) = 1) /\ forall pfa_factor_left_associativity_prime pfa_factor_right_associativity_prime. (p) = pfa_factor_left_associativity_prime * pfa_factor_right_associativity_prime -> pfa_factor_left_associativity_prime = 1 \/ pfa_factor_right_associativity_prime = 1) -> (((forall fom_index_pfp_associativity_ABleft. (exists fom_gap_pfp_associativity_ABleft_index_bound. fom_gap_pfp_associativity_ABleft_index_bound + S (fom_index_pfp_associativity_ABleft) = L) -> exists fom_value_pfp_associativity_ABleft. ((((exists fom_beta_height_pfp_associativity_ABleft_entry. fom_beta_height_pfp_associativity_ABleft_entry + S (fom_value_pfp_associativity_ABleft) = S ((S (fom_index_pfp_associativity_ABleft)) * ac)) /\ exists fom_beta_quotient_pfp_associativity_ABleft_entry. ab = fom_beta_quotient_pfp_associativity_ABleft_entry * S ((S (fom_index_pfp_associativity_ABleft)) * ac) + (fom_value_pfp_associativity_ABleft))) /\ (exists fom_gap_pfp_associativity_ABleft_value_bound. fom_gap_pfp_associativity_ABleft_value_bound + S (fom_value_pfp_associativity_ABleft) = p))) /\ (((forall fom_index_pfp_associativity_ABright. (exists fom_gap_pfp_associativity_ABright_index_bound. fom_gap_pfp_associativity_ABright_index_bound + S (fom_index_pfp_associativity_ABright) = M) -> exists fom_value_pfp_associativity_ABright. ((((exists fom_beta_height_pfp_associativity_ABright_entry. fom_beta_height_pfp_associativity_ABright_entry + S (fom_value_pfp_associativity_ABright) = S ((S (fom_index_pfp_associativity_ABright)) * bc)) /\ exists fom_beta_quotient_pfp_associativity_ABright_entry. bb = fom_beta_quotient_pfp_associativity_ABright_entry * S ((S (fom_index_pfp_associativity_ABright)) * bc) + (fom_value_pfp_associativity_ABright))) /\ (exists fom_gap_pfp_associativity_ABright_value_bound. fom_gap_pfp_associativity_ABright_value_bound + S (fom_value_pfp_associativity_ABright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_associativity_ABcoefficients. (exists pfa_gap_associativity_ABcoefficientsbound. pfa_gap_associativity_ABcoefficientsbound + S (pfc_index_associativity_ABcoefficients) = (N)) -> exists pfc_value_associativity_ABcoefficients. ((((exists ff_h_pfp_associativity_ABcoefficientsentry. ff_h_pfp_associativity_ABcoefficientsentry + S (pfc_value_associativity_ABcoefficients) = S ((S (pfc_index_associativity_ABcoefficients)) * pc)) /\ exists ff_q_pfp_associativity_ABcoefficientsentry. pb = ff_q_pfp_associativity_ABcoefficientsentry * S ((S (pfc_index_associativity_ABcoefficients)) * pc) + (pfc_value_associativity_ABcoefficients))) /\ ((exists pfc_terms_code_associativity_ABcoefficientscoefficient pfc_terms_scale_associativity_ABcoefficientscoefficient pfc_natural_sum_associativity_ABcoefficientscoefficient. ((forall pfc_index_associativity_ABcoefficientscoefficientdiagonal. (exists pfa_gap_associativity_ABcoefficientscoefficientdiagonalbound. pfa_gap_associativity_ABcoefficientscoefficientdiagonalbound + S (pfc_index_associativity_ABcoefficientscoefficientdiagonal) = (S (pfc_index_associativity_ABcoefficients))) -> exists pfc_value_associativity_ABcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associativity_ABcoefficientscoefficientdiagonalentry. ff_h_pfp_associativity_ABcoefficientscoefficientdiagonalentry + S (pfc_value_associativity_ABcoefficientscoefficientdiagonal) = S ((S (pfc_index_associativity_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_ABcoefficientscoefficient)) /\ exists ff_q_pfp_associativity_ABcoefficientscoefficientdiagonalentry. pfc_terms_code_associativity_ABcoefficientscoefficient = ff_q_pfp_associativity_ABcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associativity_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_ABcoefficientscoefficient) + (pfc_value_associativity_ABcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associativity_ABcoefficientscoefficientdiagonalterm pfc_left_associativity_ABcoefficientscoefficientdiagonalterm pfc_right_associativity_ABcoefficientscoefficientdiagonalterm. (((pfc_index_associativity_ABcoefficientscoefficientdiagonal)+pfc_complement_associativity_ABcoefficientscoefficientdiagonalterm=(pfc_index_associativity_ABcoefficients)) /\ ((((((exists pfa_gap_associativity_ABcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associativity_ABcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associativity_ABcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_associativity_ABcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associativity_ABcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associativity_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associativity_ABcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_associativity_ABcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_associativity_ABcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associativity_ABcoefficientscoefficientdiagonal)) * ac) + (pfc_left_associativity_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_ABcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associativity_ABcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_associativity_ABcoefficientscoefficientdiagonal)) /\ (((pfc_left_associativity_ABcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associativity_ABcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associativity_ABcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associativity_ABcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_associativity_ABcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associativity_ABcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associativity_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associativity_ABcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_associativity_ABcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_associativity_ABcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associativity_ABcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_associativity_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_ABcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associativity_ABcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_associativity_ABcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associativity_ABcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associativity_ABcoefficientscoefficientdiagonal)=pfc_left_associativity_ABcoefficientscoefficientdiagonalterm*pfc_right_associativity_ABcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associativity_ABcoefficientscoefficientsum fs_v_pfc_associativity_ABcoefficientscoefficientsum. ((((exists fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_start. fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associativity_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_start. fs_u_pfc_associativity_ABcoefficientscoefficientsum = fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associativity_ABcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_terminal. fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associativity_ABcoefficientscoefficient) = S ((S (S (pfc_index_associativity_ABcoefficients))) * fs_v_pfc_associativity_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_terminal. fs_u_pfc_associativity_ABcoefficientscoefficientsum = fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associativity_ABcoefficients))) * fs_v_pfc_associativity_ABcoefficientscoefficientsum) + (pfc_natural_sum_associativity_ABcoefficientscoefficient))) /\ forall fs_i_pfc_associativity_ABcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associativity_ABcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associativity_ABcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associativity_ABcoefficientscoefficientsum_body_steps = S (pfc_index_associativity_ABcoefficients)) -> exists fs_a_pfc_associativity_ABcoefficientscoefficientsum_body_steps fs_r_pfc_associativity_ABcoefficientscoefficientsum_body_steps fs_s_pfc_associativity_ABcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associativity_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_ABcoefficientscoefficient)) /\ exists fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associativity_ABcoefficientscoefficient = fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associativity_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_ABcoefficientscoefficient) + (fs_a_pfc_associativity_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associativity_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associativity_ABcoefficientscoefficientsum = fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associativity_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_ABcoefficientscoefficientsum) + (fs_r_pfc_associativity_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associativity_ABcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associativity_ABcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associativity_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associativity_ABcoefficientscoefficientsum = fs_q_pfc_associativity_ABcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associativity_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_ABcoefficientscoefficientsum) + (fs_s_pfc_associativity_ABcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associativity_ABcoefficientscoefficientsum_body_steps = fs_r_pfc_associativity_ABcoefficientscoefficientsum_body_steps + fs_a_pfc_associativity_ABcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associativity_ABcoefficientscoefficientresiduebound. pfa_gap_associativity_ABcoefficientscoefficientresiduebound + S (pfc_value_associativity_ABcoefficients) = (p)) /\ ((exists pfa_offset_left_associativity_ABcoefficientscoefficientresiduecongruence pfa_offset_right_associativity_ABcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associativity_ABcoefficientscoefficient) + (p) * pfa_offset_left_associativity_ABcoefficientscoefficientresiduecongruence = (pfc_value_associativity_ABcoefficients) + (p) * pfa_offset_right_associativity_ABcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_associativity_BCleft. (exists fom_gap_pfp_associativity_BCleft_index_bound. fom_gap_pfp_associativity_BCleft_index_bound + S (fom_index_pfp_associativity_BCleft) = M) -> exists fom_value_pfp_associativity_BCleft. ((((exists fom_beta_height_pfp_associativity_BCleft_entry. fom_beta_height_pfp_associativity_BCleft_entry + S (fom_value_pfp_associativity_BCleft) = S ((S (fom_index_pfp_associativity_BCleft)) * bc)) /\ exists fom_beta_quotient_pfp_associativity_BCleft_entry. bb = fom_beta_quotient_pfp_associativity_BCleft_entry * S ((S (fom_index_pfp_associativity_BCleft)) * bc) + (fom_value_pfp_associativity_BCleft))) /\ (exists fom_gap_pfp_associativity_BCleft_value_bound. fom_gap_pfp_associativity_BCleft_value_bound + S (fom_value_pfp_associativity_BCleft) = p))) /\ (((forall fom_index_pfp_associativity_BCright. (exists fom_gap_pfp_associativity_BCright_index_bound. fom_gap_pfp_associativity_BCright_index_bound + S (fom_index_pfp_associativity_BCright) = J) -> exists fom_value_pfp_associativity_BCright. ((((exists fom_beta_height_pfp_associativity_BCright_entry. fom_beta_height_pfp_associativity_BCright_entry + S (fom_value_pfp_associativity_BCright) = S ((S (fom_index_pfp_associativity_BCright)) * cc)) /\ exists fom_beta_quotient_pfp_associativity_BCright_entry. cb = fom_beta_quotient_pfp_associativity_BCright_entry * S ((S (fom_index_pfp_associativity_BCright)) * cc) + (fom_value_pfp_associativity_BCright))) /\ (exists fom_gap_pfp_associativity_BCright_value_bound. fom_gap_pfp_associativity_BCright_value_bound + S (fom_value_pfp_associativity_BCright) = p))) /\ (((((((M)=0 \/ (J)=0) /\ (((K)=0)))) \/ (((~((M)=0)) /\ (((~((J)=0)) /\ (((M)+(J)=S (K)))))))) /\ ((forall pfc_index_associativity_BCcoefficients. (exists pfa_gap_associativity_BCcoefficientsbound. pfa_gap_associativity_BCcoefficientsbound + S (pfc_index_associativity_BCcoefficients) = (K)) -> exists pfc_value_associativity_BCcoefficients. ((((exists ff_h_pfp_associativity_BCcoefficientsentry. ff_h_pfp_associativity_BCcoefficientsentry + S (pfc_value_associativity_BCcoefficients) = S ((S (pfc_index_associativity_BCcoefficients)) * qc)) /\ exists ff_q_pfp_associativity_BCcoefficientsentry. qb = ff_q_pfp_associativity_BCcoefficientsentry * S ((S (pfc_index_associativity_BCcoefficients)) * qc) + (pfc_value_associativity_BCcoefficients))) /\ ((exists pfc_terms_code_associativity_BCcoefficientscoefficient pfc_terms_scale_associativity_BCcoefficientscoefficient pfc_natural_sum_associativity_BCcoefficientscoefficient. ((forall pfc_index_associativity_BCcoefficientscoefficientdiagonal. (exists pfa_gap_associativity_BCcoefficientscoefficientdiagonalbound. pfa_gap_associativity_BCcoefficientscoefficientdiagonalbound + S (pfc_index_associativity_BCcoefficientscoefficientdiagonal) = (S (pfc_index_associativity_BCcoefficients))) -> exists pfc_value_associativity_BCcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associativity_BCcoefficientscoefficientdiagonalentry. ff_h_pfp_associativity_BCcoefficientscoefficientdiagonalentry + S (pfc_value_associativity_BCcoefficientscoefficientdiagonal) = S ((S (pfc_index_associativity_BCcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_BCcoefficientscoefficient)) /\ exists ff_q_pfp_associativity_BCcoefficientscoefficientdiagonalentry. pfc_terms_code_associativity_BCcoefficientscoefficient = ff_q_pfp_associativity_BCcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associativity_BCcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_BCcoefficientscoefficient) + (pfc_value_associativity_BCcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associativity_BCcoefficientscoefficientdiagonalterm pfc_left_associativity_BCcoefficientscoefficientdiagonalterm pfc_right_associativity_BCcoefficientscoefficientdiagonalterm. (((pfc_index_associativity_BCcoefficientscoefficientdiagonal)+pfc_complement_associativity_BCcoefficientscoefficientdiagonalterm=(pfc_index_associativity_BCcoefficients)) /\ ((((((exists pfa_gap_associativity_BCcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associativity_BCcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associativity_BCcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_associativity_BCcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associativity_BCcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associativity_BCcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associativity_BCcoefficientscoefficientdiagonal)) * bc)) /\ exists ff_q_pfp_associativity_BCcoefficientscoefficientdiagonaltermleftentry. bb = ff_q_pfp_associativity_BCcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associativity_BCcoefficientscoefficientdiagonal)) * bc) + (pfc_left_associativity_BCcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_BCcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associativity_BCcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_associativity_BCcoefficientscoefficientdiagonal)) /\ (((pfc_left_associativity_BCcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associativity_BCcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associativity_BCcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associativity_BCcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_associativity_BCcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associativity_BCcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associativity_BCcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associativity_BCcoefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_associativity_BCcoefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_associativity_BCcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associativity_BCcoefficientscoefficientdiagonalterm)) * cc) + (pfc_right_associativity_BCcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_BCcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associativity_BCcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_associativity_BCcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associativity_BCcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associativity_BCcoefficientscoefficientdiagonal)=pfc_left_associativity_BCcoefficientscoefficientdiagonalterm*pfc_right_associativity_BCcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associativity_BCcoefficientscoefficientsum fs_v_pfc_associativity_BCcoefficientscoefficientsum. ((((exists fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_start. fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associativity_BCcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_start. fs_u_pfc_associativity_BCcoefficientscoefficientsum = fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associativity_BCcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_terminal. fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associativity_BCcoefficientscoefficient) = S ((S (S (pfc_index_associativity_BCcoefficients))) * fs_v_pfc_associativity_BCcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_terminal. fs_u_pfc_associativity_BCcoefficientscoefficientsum = fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associativity_BCcoefficients))) * fs_v_pfc_associativity_BCcoefficientscoefficientsum) + (pfc_natural_sum_associativity_BCcoefficientscoefficient))) /\ forall fs_i_pfc_associativity_BCcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associativity_BCcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associativity_BCcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associativity_BCcoefficientscoefficientsum_body_steps = S (pfc_index_associativity_BCcoefficients)) -> exists fs_a_pfc_associativity_BCcoefficientscoefficientsum_body_steps fs_r_pfc_associativity_BCcoefficientscoefficientsum_body_steps fs_s_pfc_associativity_BCcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associativity_BCcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_BCcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_BCcoefficientscoefficient)) /\ exists fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associativity_BCcoefficientscoefficient = fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associativity_BCcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_BCcoefficientscoefficient) + (fs_a_pfc_associativity_BCcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associativity_BCcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_BCcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_BCcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associativity_BCcoefficientscoefficientsum = fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associativity_BCcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_BCcoefficientscoefficientsum) + (fs_r_pfc_associativity_BCcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associativity_BCcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associativity_BCcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associativity_BCcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_BCcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associativity_BCcoefficientscoefficientsum = fs_q_pfc_associativity_BCcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associativity_BCcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_BCcoefficientscoefficientsum) + (fs_s_pfc_associativity_BCcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associativity_BCcoefficientscoefficientsum_body_steps = fs_r_pfc_associativity_BCcoefficientscoefficientsum_body_steps + fs_a_pfc_associativity_BCcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associativity_BCcoefficientscoefficientresiduebound. pfa_gap_associativity_BCcoefficientscoefficientresiduebound + S (pfc_value_associativity_BCcoefficients) = (p)) /\ ((exists pfa_offset_left_associativity_BCcoefficientscoefficientresiduecongruence pfa_offset_right_associativity_BCcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associativity_BCcoefficientscoefficient) + (p) * pfa_offset_left_associativity_BCcoefficientscoefficientresiduecongruence = (pfc_value_associativity_BCcoefficients) + (p) * pfa_offset_right_associativity_BCcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_associativity_PCleft. (exists fom_gap_pfp_associativity_PCleft_index_bound. fom_gap_pfp_associativity_PCleft_index_bound + S (fom_index_pfp_associativity_PCleft) = N) -> exists fom_value_pfp_associativity_PCleft. ((((exists fom_beta_height_pfp_associativity_PCleft_entry. fom_beta_height_pfp_associativity_PCleft_entry + S (fom_value_pfp_associativity_PCleft) = S ((S (fom_index_pfp_associativity_PCleft)) * pc)) /\ exists fom_beta_quotient_pfp_associativity_PCleft_entry. pb = fom_beta_quotient_pfp_associativity_PCleft_entry * S ((S (fom_index_pfp_associativity_PCleft)) * pc) + (fom_value_pfp_associativity_PCleft))) /\ (exists fom_gap_pfp_associativity_PCleft_value_bound. fom_gap_pfp_associativity_PCleft_value_bound + S (fom_value_pfp_associativity_PCleft) = p))) /\ (((forall fom_index_pfp_associativity_PCright. (exists fom_gap_pfp_associativity_PCright_index_bound. fom_gap_pfp_associativity_PCright_index_bound + S (fom_index_pfp_associativity_PCright) = J) -> exists fom_value_pfp_associativity_PCright. ((((exists fom_beta_height_pfp_associativity_PCright_entry. fom_beta_height_pfp_associativity_PCright_entry + S (fom_value_pfp_associativity_PCright) = S ((S (fom_index_pfp_associativity_PCright)) * cc)) /\ exists fom_beta_quotient_pfp_associativity_PCright_entry. cb = fom_beta_quotient_pfp_associativity_PCright_entry * S ((S (fom_index_pfp_associativity_PCright)) * cc) + (fom_value_pfp_associativity_PCright))) /\ (exists fom_gap_pfp_associativity_PCright_value_bound. fom_gap_pfp_associativity_PCright_value_bound + S (fom_value_pfp_associativity_PCright) = p))) /\ (((((((N)=0 \/ (J)=0) /\ (((U)=0)))) \/ (((~((N)=0)) /\ (((~((J)=0)) /\ (((N)+(J)=S (U)))))))) /\ ((forall pfc_index_associativity_PCcoefficients. (exists pfa_gap_associativity_PCcoefficientsbound. pfa_gap_associativity_PCcoefficientsbound + S (pfc_index_associativity_PCcoefficients) = (U)) -> exists pfc_value_associativity_PCcoefficients. ((((exists ff_h_pfp_associativity_PCcoefficientsentry. ff_h_pfp_associativity_PCcoefficientsentry + S (pfc_value_associativity_PCcoefficients) = S ((S (pfc_index_associativity_PCcoefficients)) * rc)) /\ exists ff_q_pfp_associativity_PCcoefficientsentry. rb = ff_q_pfp_associativity_PCcoefficientsentry * S ((S (pfc_index_associativity_PCcoefficients)) * rc) + (pfc_value_associativity_PCcoefficients))) /\ ((exists pfc_terms_code_associativity_PCcoefficientscoefficient pfc_terms_scale_associativity_PCcoefficientscoefficient pfc_natural_sum_associativity_PCcoefficientscoefficient. ((forall pfc_index_associativity_PCcoefficientscoefficientdiagonal. (exists pfa_gap_associativity_PCcoefficientscoefficientdiagonalbound. pfa_gap_associativity_PCcoefficientscoefficientdiagonalbound + S (pfc_index_associativity_PCcoefficientscoefficientdiagonal) = (S (pfc_index_associativity_PCcoefficients))) -> exists pfc_value_associativity_PCcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associativity_PCcoefficientscoefficientdiagonalentry. ff_h_pfp_associativity_PCcoefficientscoefficientdiagonalentry + S (pfc_value_associativity_PCcoefficientscoefficientdiagonal) = S ((S (pfc_index_associativity_PCcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_PCcoefficientscoefficient)) /\ exists ff_q_pfp_associativity_PCcoefficientscoefficientdiagonalentry. pfc_terms_code_associativity_PCcoefficientscoefficient = ff_q_pfp_associativity_PCcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associativity_PCcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_PCcoefficientscoefficient) + (pfc_value_associativity_PCcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associativity_PCcoefficientscoefficientdiagonalterm pfc_left_associativity_PCcoefficientscoefficientdiagonalterm pfc_right_associativity_PCcoefficientscoefficientdiagonalterm. (((pfc_index_associativity_PCcoefficientscoefficientdiagonal)+pfc_complement_associativity_PCcoefficientscoefficientdiagonalterm=(pfc_index_associativity_PCcoefficients)) /\ ((((((exists pfa_gap_associativity_PCcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associativity_PCcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associativity_PCcoefficientscoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_associativity_PCcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associativity_PCcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associativity_PCcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associativity_PCcoefficientscoefficientdiagonal)) * pc)) /\ exists ff_q_pfp_associativity_PCcoefficientscoefficientdiagonaltermleftentry. pb = ff_q_pfp_associativity_PCcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associativity_PCcoefficientscoefficientdiagonal)) * pc) + (pfc_left_associativity_PCcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_PCcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associativity_PCcoefficientscoefficientdiagonaltermleftoutside+(N)=(pfc_index_associativity_PCcoefficientscoefficientdiagonal)) /\ (((pfc_left_associativity_PCcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associativity_PCcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associativity_PCcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associativity_PCcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_associativity_PCcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associativity_PCcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associativity_PCcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associativity_PCcoefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_associativity_PCcoefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_associativity_PCcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associativity_PCcoefficientscoefficientdiagonalterm)) * cc) + (pfc_right_associativity_PCcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_PCcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associativity_PCcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_associativity_PCcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associativity_PCcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associativity_PCcoefficientscoefficientdiagonal)=pfc_left_associativity_PCcoefficientscoefficientdiagonalterm*pfc_right_associativity_PCcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associativity_PCcoefficientscoefficientsum fs_v_pfc_associativity_PCcoefficientscoefficientsum. ((((exists fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_start. fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associativity_PCcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_start. fs_u_pfc_associativity_PCcoefficientscoefficientsum = fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associativity_PCcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_terminal. fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associativity_PCcoefficientscoefficient) = S ((S (S (pfc_index_associativity_PCcoefficients))) * fs_v_pfc_associativity_PCcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_terminal. fs_u_pfc_associativity_PCcoefficientscoefficientsum = fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associativity_PCcoefficients))) * fs_v_pfc_associativity_PCcoefficientscoefficientsum) + (pfc_natural_sum_associativity_PCcoefficientscoefficient))) /\ forall fs_i_pfc_associativity_PCcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associativity_PCcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associativity_PCcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associativity_PCcoefficientscoefficientsum_body_steps = S (pfc_index_associativity_PCcoefficients)) -> exists fs_a_pfc_associativity_PCcoefficientscoefficientsum_body_steps fs_r_pfc_associativity_PCcoefficientscoefficientsum_body_steps fs_s_pfc_associativity_PCcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associativity_PCcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_PCcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_PCcoefficientscoefficient)) /\ exists fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associativity_PCcoefficientscoefficient = fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associativity_PCcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_PCcoefficientscoefficient) + (fs_a_pfc_associativity_PCcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associativity_PCcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_PCcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_PCcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associativity_PCcoefficientscoefficientsum = fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associativity_PCcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_PCcoefficientscoefficientsum) + (fs_r_pfc_associativity_PCcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associativity_PCcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associativity_PCcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associativity_PCcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_PCcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associativity_PCcoefficientscoefficientsum = fs_q_pfc_associativity_PCcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associativity_PCcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_PCcoefficientscoefficientsum) + (fs_s_pfc_associativity_PCcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associativity_PCcoefficientscoefficientsum_body_steps = fs_r_pfc_associativity_PCcoefficientscoefficientsum_body_steps + fs_a_pfc_associativity_PCcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associativity_PCcoefficientscoefficientresiduebound. pfa_gap_associativity_PCcoefficientscoefficientresiduebound + S (pfc_value_associativity_PCcoefficients) = (p)) /\ ((exists pfa_offset_left_associativity_PCcoefficientscoefficientresiduecongruence pfa_offset_right_associativity_PCcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associativity_PCcoefficientscoefficient) + (p) * pfa_offset_left_associativity_PCcoefficientscoefficientresiduecongruence = (pfc_value_associativity_PCcoefficients) + (p) * pfa_offset_right_associativity_PCcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_associativity_AQleft. (exists fom_gap_pfp_associativity_AQleft_index_bound. fom_gap_pfp_associativity_AQleft_index_bound + S (fom_index_pfp_associativity_AQleft) = L) -> exists fom_value_pfp_associativity_AQleft. ((((exists fom_beta_height_pfp_associativity_AQleft_entry. fom_beta_height_pfp_associativity_AQleft_entry + S (fom_value_pfp_associativity_AQleft) = S ((S (fom_index_pfp_associativity_AQleft)) * ac)) /\ exists fom_beta_quotient_pfp_associativity_AQleft_entry. ab = fom_beta_quotient_pfp_associativity_AQleft_entry * S ((S (fom_index_pfp_associativity_AQleft)) * ac) + (fom_value_pfp_associativity_AQleft))) /\ (exists fom_gap_pfp_associativity_AQleft_value_bound. fom_gap_pfp_associativity_AQleft_value_bound + S (fom_value_pfp_associativity_AQleft) = p))) /\ (((forall fom_index_pfp_associativity_AQright. (exists fom_gap_pfp_associativity_AQright_index_bound. fom_gap_pfp_associativity_AQright_index_bound + S (fom_index_pfp_associativity_AQright) = K) -> exists fom_value_pfp_associativity_AQright. ((((exists fom_beta_height_pfp_associativity_AQright_entry. fom_beta_height_pfp_associativity_AQright_entry + S (fom_value_pfp_associativity_AQright) = S ((S (fom_index_pfp_associativity_AQright)) * qc)) /\ exists fom_beta_quotient_pfp_associativity_AQright_entry. qb = fom_beta_quotient_pfp_associativity_AQright_entry * S ((S (fom_index_pfp_associativity_AQright)) * qc) + (fom_value_pfp_associativity_AQright))) /\ (exists fom_gap_pfp_associativity_AQright_value_bound. fom_gap_pfp_associativity_AQright_value_bound + S (fom_value_pfp_associativity_AQright) = p))) /\ (((((((L)=0 \/ (K)=0) /\ (((V)=0)))) \/ (((~((L)=0)) /\ (((~((K)=0)) /\ (((L)+(K)=S (V)))))))) /\ ((forall pfc_index_associativity_AQcoefficients. (exists pfa_gap_associativity_AQcoefficientsbound. pfa_gap_associativity_AQcoefficientsbound + S (pfc_index_associativity_AQcoefficients) = (V)) -> exists pfc_value_associativity_AQcoefficients. ((((exists ff_h_pfp_associativity_AQcoefficientsentry. ff_h_pfp_associativity_AQcoefficientsentry + S (pfc_value_associativity_AQcoefficients) = S ((S (pfc_index_associativity_AQcoefficients)) * sc)) /\ exists ff_q_pfp_associativity_AQcoefficientsentry. sb = ff_q_pfp_associativity_AQcoefficientsentry * S ((S (pfc_index_associativity_AQcoefficients)) * sc) + (pfc_value_associativity_AQcoefficients))) /\ ((exists pfc_terms_code_associativity_AQcoefficientscoefficient pfc_terms_scale_associativity_AQcoefficientscoefficient pfc_natural_sum_associativity_AQcoefficientscoefficient. ((forall pfc_index_associativity_AQcoefficientscoefficientdiagonal. (exists pfa_gap_associativity_AQcoefficientscoefficientdiagonalbound. pfa_gap_associativity_AQcoefficientscoefficientdiagonalbound + S (pfc_index_associativity_AQcoefficientscoefficientdiagonal) = (S (pfc_index_associativity_AQcoefficients))) -> exists pfc_value_associativity_AQcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associativity_AQcoefficientscoefficientdiagonalentry. ff_h_pfp_associativity_AQcoefficientscoefficientdiagonalentry + S (pfc_value_associativity_AQcoefficientscoefficientdiagonal) = S ((S (pfc_index_associativity_AQcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_AQcoefficientscoefficient)) /\ exists ff_q_pfp_associativity_AQcoefficientscoefficientdiagonalentry. pfc_terms_code_associativity_AQcoefficientscoefficient = ff_q_pfp_associativity_AQcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associativity_AQcoefficientscoefficientdiagonal)) * pfc_terms_scale_associativity_AQcoefficientscoefficient) + (pfc_value_associativity_AQcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associativity_AQcoefficientscoefficientdiagonalterm pfc_left_associativity_AQcoefficientscoefficientdiagonalterm pfc_right_associativity_AQcoefficientscoefficientdiagonalterm. (((pfc_index_associativity_AQcoefficientscoefficientdiagonal)+pfc_complement_associativity_AQcoefficientscoefficientdiagonalterm=(pfc_index_associativity_AQcoefficients)) /\ ((((((exists pfa_gap_associativity_AQcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associativity_AQcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associativity_AQcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_associativity_AQcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associativity_AQcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associativity_AQcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associativity_AQcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_associativity_AQcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_associativity_AQcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associativity_AQcoefficientscoefficientdiagonal)) * ac) + (pfc_left_associativity_AQcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_AQcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associativity_AQcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_associativity_AQcoefficientscoefficientdiagonal)) /\ (((pfc_left_associativity_AQcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associativity_AQcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associativity_AQcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associativity_AQcoefficientscoefficientdiagonalterm) = (K)) /\ ((((exists ff_h_pfp_associativity_AQcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associativity_AQcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associativity_AQcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associativity_AQcoefficientscoefficientdiagonalterm)) * qc)) /\ exists ff_q_pfp_associativity_AQcoefficientscoefficientdiagonaltermrightentry. qb = ff_q_pfp_associativity_AQcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associativity_AQcoefficientscoefficientdiagonalterm)) * qc) + (pfc_right_associativity_AQcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associativity_AQcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associativity_AQcoefficientscoefficientdiagonaltermrightoutside+(K)=(pfc_complement_associativity_AQcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associativity_AQcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associativity_AQcoefficientscoefficientdiagonal)=pfc_left_associativity_AQcoefficientscoefficientdiagonalterm*pfc_right_associativity_AQcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associativity_AQcoefficientscoefficientsum fs_v_pfc_associativity_AQcoefficientscoefficientsum. ((((exists fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_start. fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associativity_AQcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_start. fs_u_pfc_associativity_AQcoefficientscoefficientsum = fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associativity_AQcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_terminal. fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associativity_AQcoefficientscoefficient) = S ((S (S (pfc_index_associativity_AQcoefficients))) * fs_v_pfc_associativity_AQcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_terminal. fs_u_pfc_associativity_AQcoefficientscoefficientsum = fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associativity_AQcoefficients))) * fs_v_pfc_associativity_AQcoefficientscoefficientsum) + (pfc_natural_sum_associativity_AQcoefficientscoefficient))) /\ forall fs_i_pfc_associativity_AQcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associativity_AQcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associativity_AQcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associativity_AQcoefficientscoefficientsum_body_steps = S (pfc_index_associativity_AQcoefficients)) -> exists fs_a_pfc_associativity_AQcoefficientscoefficientsum_body_steps fs_r_pfc_associativity_AQcoefficientscoefficientsum_body_steps fs_s_pfc_associativity_AQcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associativity_AQcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_AQcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_AQcoefficientscoefficient)) /\ exists fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associativity_AQcoefficientscoefficient = fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associativity_AQcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associativity_AQcoefficientscoefficient) + (fs_a_pfc_associativity_AQcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associativity_AQcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associativity_AQcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_AQcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associativity_AQcoefficientscoefficientsum = fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associativity_AQcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_AQcoefficientscoefficientsum) + (fs_r_pfc_associativity_AQcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associativity_AQcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associativity_AQcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associativity_AQcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_AQcoefficientscoefficientsum)) /\ exists fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associativity_AQcoefficientscoefficientsum = fs_q_pfc_associativity_AQcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associativity_AQcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associativity_AQcoefficientscoefficientsum) + (fs_s_pfc_associativity_AQcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associativity_AQcoefficientscoefficientsum_body_steps = fs_r_pfc_associativity_AQcoefficientscoefficientsum_body_steps + fs_a_pfc_associativity_AQcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associativity_AQcoefficientscoefficientresiduebound. pfa_gap_associativity_AQcoefficientscoefficientresiduebound + S (pfc_value_associativity_AQcoefficients) = (p)) /\ ((exists pfa_offset_left_associativity_AQcoefficientscoefficientresiduecongruence pfa_offset_right_associativity_AQcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associativity_AQcoefficientscoefficient) + (p) * pfa_offset_left_associativity_AQcoefficientscoefficientresiduecongruence = (pfc_value_associativity_AQcoefficients) + (p) * pfa_offset_right_associativity_AQcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_associativity_result pfrep_left_associativity_result pfrep_right_associativity_result. ((exists pfrep_position_associativity_resultfirst. ((pfrep_position_associativity_resultfirst+S (pfrep_power_associativity_result)=(U)) /\ ((((exists ff_h_pfp_associativity_resultfirstentry. ff_h_pfp_associativity_resultfirstentry + S (pfrep_left_associativity_result) = S ((S (pfrep_position_associativity_resultfirst)) * rc)) /\ exists ff_q_pfp_associativity_resultfirstentry. rb = ff_q_pfp_associativity_resultfirstentry * S ((S (pfrep_position_associativity_resultfirst)) * rc) + (pfrep_left_associativity_result)))))) \/ (((exists pfrep_gap_associativity_resultfirstoutside. pfrep_gap_associativity_resultfirstoutside+(U)=(pfrep_power_associativity_result)) /\ (((pfrep_left_associativity_result)=0))))) -> ((exists pfrep_position_associativity_resultsecond. ((pfrep_position_associativity_resultsecond+S (pfrep_power_associativity_result)=(V)) /\ ((((exists ff_h_pfp_associativity_resultsecondentry. ff_h_pfp_associativity_resultsecondentry + S (pfrep_right_associativity_result) = S ((S (pfrep_position_associativity_resultsecond)) * sc)) /\ exists ff_q_pfp_associativity_resultsecondentry. sb = ff_q_pfp_associativity_resultsecondentry * S ((S (pfrep_position_associativity_resultsecond)) * sc) + (pfrep_right_associativity_result)))))) \/ (((exists pfrep_gap_associativity_resultsecondoutside. pfrep_gap_associativity_resultsecondoutside+(V)=(pfrep_power_associativity_result)) /\ (((pfrep_right_associativity_result)=0))))) -> pfrep_left_associativity_result=pfrep_right_associativity_result)
Complete tactic proof in conservative notation
All 283 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.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank bounded prefix drop last.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.