Actual left products distribute over an independently represented aligned sum: construct real equal-length products of its witnesses and prove formal equivalence to the three supplied outputs, including empty-factor cases.
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 ub uc L vb vc M wb wc N db dc J pb pc H qb qc I rb rc K. (~((p) = 1) /\ forall pfa_factor_left_aligned_left_prime pfa_factor_right_aligned_left_prime. (p) = pfa_factor_left_aligned_left_prime * pfa_factor_right_aligned_left_prime -> pfa_factor_left_aligned_left_prime = 1 \/ pfa_factor_right_aligned_left_prime = 1) -> (((forall fom_index_pfp_aligned_left_input_left_bounded. (exists fom_gap_pfp_aligned_left_input_left_bounded_index_bound. fom_gap_pfp_aligned_left_input_left_bounded_index_bound + S (fom_index_pfp_aligned_left_input_left_bounded) = L) -> exists fom_value_pfp_aligned_left_input_left_bounded. ((((exists fom_beta_height_pfp_aligned_left_input_left_bounded_entry. fom_beta_height_pfp_aligned_left_input_left_bounded_entry + S (fom_value_pfp_aligned_left_input_left_bounded) = S ((S (fom_index_pfp_aligned_left_input_left_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_aligned_left_input_left_bounded_entry. ub = fom_beta_quotient_pfp_aligned_left_input_left_bounded_entry * S ((S (fom_index_pfp_aligned_left_input_left_bounded)) * uc) + (fom_value_pfp_aligned_left_input_left_bounded))) /\ (exists fom_gap_pfp_aligned_left_input_left_bounded_value_bound. fom_gap_pfp_aligned_left_input_left_bounded_value_bound + S (fom_value_pfp_aligned_left_input_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_left_input_right_bounded. (exists fom_gap_pfp_aligned_left_input_right_bounded_index_bound. fom_gap_pfp_aligned_left_input_right_bounded_index_bound + S (fom_index_pfp_aligned_left_input_right_bounded) = M) -> exists fom_value_pfp_aligned_left_input_right_bounded. ((((exists fom_beta_height_pfp_aligned_left_input_right_bounded_entry. fom_beta_height_pfp_aligned_left_input_right_bounded_entry + S (fom_value_pfp_aligned_left_input_right_bounded) = S ((S (fom_index_pfp_aligned_left_input_right_bounded)) * vc)) /\ exists fom_beta_quotient_pfp_aligned_left_input_right_bounded_entry. vb = fom_beta_quotient_pfp_aligned_left_input_right_bounded_entry * S ((S (fom_index_pfp_aligned_left_input_right_bounded)) * vc) + (fom_value_pfp_aligned_left_input_right_bounded))) /\ (exists fom_gap_pfp_aligned_left_input_right_bounded_value_bound. fom_gap_pfp_aligned_left_input_right_bounded_value_bound + S (fom_value_pfp_aligned_left_input_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_left_input_result_bounded. (exists fom_gap_pfp_aligned_left_input_result_bounded_index_bound. fom_gap_pfp_aligned_left_input_result_bounded_index_bound + S (fom_index_pfp_aligned_left_input_result_bounded) = N) -> exists fom_value_pfp_aligned_left_input_result_bounded. ((((exists fom_beta_height_pfp_aligned_left_input_result_bounded_entry. fom_beta_height_pfp_aligned_left_input_result_bounded_entry + S (fom_value_pfp_aligned_left_input_result_bounded) = S ((S (fom_index_pfp_aligned_left_input_result_bounded)) * wc)) /\ exists fom_beta_quotient_pfp_aligned_left_input_result_bounded_entry. wb = fom_beta_quotient_pfp_aligned_left_input_result_bounded_entry * S ((S (fom_index_pfp_aligned_left_input_result_bounded)) * wc) + (fom_value_pfp_aligned_left_input_result_bounded))) /\ (exists fom_gap_pfp_aligned_left_input_result_bounded_value_bound. fom_gap_pfp_aligned_left_input_result_bounded_value_bound + S (fom_value_pfp_aligned_left_input_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_left_input pfaa_left_c_aligned_left_input pfaa_right_b_aligned_left_input pfaa_right_c_aligned_left_input pfaa_sum_b_aligned_left_input pfaa_sum_c_aligned_left_input pfaa_length_aligned_left_input. ((((forall pfrep_power_aligned_left_input_witness_common_left pfrep_left_aligned_left_input_witness_common_left pfrep_right_aligned_left_input_witness_common_left. ((exists pfrep_position_aligned_left_input_witness_common_leftfirst. ((pfrep_position_aligned_left_input_witness_common_leftfirst+S (pfrep_power_aligned_left_input_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_aligned_left_input_witness_common_leftfirstentry. ff_h_pfp_aligned_left_input_witness_common_leftfirstentry + S (pfrep_left_aligned_left_input_witness_common_left) = S ((S (pfrep_position_aligned_left_input_witness_common_leftfirst)) * uc)) /\ exists ff_q_pfp_aligned_left_input_witness_common_leftfirstentry. ub = ff_q_pfp_aligned_left_input_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_left_input_witness_common_leftfirst)) * uc) + (pfrep_left_aligned_left_input_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_left_input_witness_common_leftfirstoutside. pfrep_gap_aligned_left_input_witness_common_leftfirstoutside+(L)=(pfrep_power_aligned_left_input_witness_common_left)) /\ (((pfrep_left_aligned_left_input_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_left_input_witness_common_leftsecond. ((pfrep_position_aligned_left_input_witness_common_leftsecond+S (pfrep_power_aligned_left_input_witness_common_left)=(pfaa_length_aligned_left_input)) /\ ((((exists ff_h_pfp_aligned_left_input_witness_common_leftsecondentry. ff_h_pfp_aligned_left_input_witness_common_leftsecondentry + S (pfrep_right_aligned_left_input_witness_common_left) = S ((S (pfrep_position_aligned_left_input_witness_common_leftsecond)) * pfaa_left_c_aligned_left_input)) /\ exists ff_q_pfp_aligned_left_input_witness_common_leftsecondentry. pfaa_left_b_aligned_left_input = ff_q_pfp_aligned_left_input_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_left_input_witness_common_leftsecond)) * pfaa_left_c_aligned_left_input) + (pfrep_right_aligned_left_input_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_left_input_witness_common_leftsecondoutside. pfrep_gap_aligned_left_input_witness_common_leftsecondoutside+(pfaa_length_aligned_left_input)=(pfrep_power_aligned_left_input_witness_common_left)) /\ (((pfrep_right_aligned_left_input_witness_common_left)=0))))) -> pfrep_left_aligned_left_input_witness_common_left=pfrep_right_aligned_left_input_witness_common_left) /\ ((forall pfrep_power_aligned_left_input_witness_common_right pfrep_left_aligned_left_input_witness_common_right pfrep_right_aligned_left_input_witness_common_right. ((exists pfrep_position_aligned_left_input_witness_common_rightfirst. ((pfrep_position_aligned_left_input_witness_common_rightfirst+S (pfrep_power_aligned_left_input_witness_common_right)=(M)) /\ ((((exists ff_h_pfp_aligned_left_input_witness_common_rightfirstentry. ff_h_pfp_aligned_left_input_witness_common_rightfirstentry + S (pfrep_left_aligned_left_input_witness_common_right) = S ((S (pfrep_position_aligned_left_input_witness_common_rightfirst)) * vc)) /\ exists ff_q_pfp_aligned_left_input_witness_common_rightfirstentry. vb = ff_q_pfp_aligned_left_input_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_left_input_witness_common_rightfirst)) * vc) + (pfrep_left_aligned_left_input_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_left_input_witness_common_rightfirstoutside. pfrep_gap_aligned_left_input_witness_common_rightfirstoutside+(M)=(pfrep_power_aligned_left_input_witness_common_right)) /\ (((pfrep_left_aligned_left_input_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_left_input_witness_common_rightsecond. ((pfrep_position_aligned_left_input_witness_common_rightsecond+S (pfrep_power_aligned_left_input_witness_common_right)=(pfaa_length_aligned_left_input)) /\ ((((exists ff_h_pfp_aligned_left_input_witness_common_rightsecondentry. ff_h_pfp_aligned_left_input_witness_common_rightsecondentry + S (pfrep_right_aligned_left_input_witness_common_right) = S ((S (pfrep_position_aligned_left_input_witness_common_rightsecond)) * pfaa_right_c_aligned_left_input)) /\ exists ff_q_pfp_aligned_left_input_witness_common_rightsecondentry. pfaa_right_b_aligned_left_input = ff_q_pfp_aligned_left_input_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_left_input_witness_common_rightsecond)) * pfaa_right_c_aligned_left_input) + (pfrep_right_aligned_left_input_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_left_input_witness_common_rightsecondoutside. pfrep_gap_aligned_left_input_witness_common_rightsecondoutside+(pfaa_length_aligned_left_input)=(pfrep_power_aligned_left_input_witness_common_right)) /\ (((pfrep_right_aligned_left_input_witness_common_right)=0))))) -> pfrep_left_aligned_left_input_witness_common_right=pfrep_right_aligned_left_input_witness_common_right)))) /\ (((forall pfp_index_aligned_left_input_witness_operation. (exists pfa_gap_aligned_left_input_witness_operationindex. pfa_gap_aligned_left_input_witness_operationindex + S (pfp_index_aligned_left_input_witness_operation) = (pfaa_length_aligned_left_input)) -> exists pfp_left_aligned_left_input_witness_operation pfp_right_aligned_left_input_witness_operation pfp_value_aligned_left_input_witness_operation. ((((exists ff_h_pfp_aligned_left_input_witness_operationleft. ff_h_pfp_aligned_left_input_witness_operationleft + S (pfp_left_aligned_left_input_witness_operation) = S ((S (pfp_index_aligned_left_input_witness_operation)) * pfaa_left_c_aligned_left_input)) /\ exists ff_q_pfp_aligned_left_input_witness_operationleft. pfaa_left_b_aligned_left_input = ff_q_pfp_aligned_left_input_witness_operationleft * S ((S (pfp_index_aligned_left_input_witness_operation)) * pfaa_left_c_aligned_left_input) + (pfp_left_aligned_left_input_witness_operation))) /\ (((((exists ff_h_pfp_aligned_left_input_witness_operationright. ff_h_pfp_aligned_left_input_witness_operationright + S (pfp_right_aligned_left_input_witness_operation) = S ((S (pfp_index_aligned_left_input_witness_operation)) * pfaa_right_c_aligned_left_input)) /\ exists ff_q_pfp_aligned_left_input_witness_operationright. pfaa_right_b_aligned_left_input = ff_q_pfp_aligned_left_input_witness_operationright * S ((S (pfp_index_aligned_left_input_witness_operation)) * pfaa_right_c_aligned_left_input) + (pfp_right_aligned_left_input_witness_operation))) /\ (((((exists ff_h_pfp_aligned_left_input_witness_operationtarget. ff_h_pfp_aligned_left_input_witness_operationtarget + S (pfp_value_aligned_left_input_witness_operation) = S ((S (pfp_index_aligned_left_input_witness_operation)) * pfaa_sum_c_aligned_left_input)) /\ exists ff_q_pfp_aligned_left_input_witness_operationtarget. pfaa_sum_b_aligned_left_input = ff_q_pfp_aligned_left_input_witness_operationtarget * S ((S (pfp_index_aligned_left_input_witness_operation)) * pfaa_sum_c_aligned_left_input) + (pfp_value_aligned_left_input_witness_operation))) /\ ((((exists pfa_gap_aligned_left_input_witness_operationoperationleft. pfa_gap_aligned_left_input_witness_operationoperationleft + S (pfp_left_aligned_left_input_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_left_input_witness_operationoperationright. pfa_gap_aligned_left_input_witness_operationoperationright + S (pfp_right_aligned_left_input_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_left_input_witness_operationoperationresultbound. pfa_gap_aligned_left_input_witness_operationoperationresultbound + S (pfp_value_aligned_left_input_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_left_input_witness_operationoperationresultcongruence pfa_offset_right_aligned_left_input_witness_operationoperationresultcongruence. ((pfp_left_aligned_left_input_witness_operation) + (pfp_right_aligned_left_input_witness_operation)) + (p) * pfa_offset_left_aligned_left_input_witness_operationoperationresultcongruence = (pfp_value_aligned_left_input_witness_operation) + (p) * pfa_offset_right_aligned_left_input_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_left_input_witness_output pfrep_left_aligned_left_input_witness_output pfrep_right_aligned_left_input_witness_output. ((exists pfrep_position_aligned_left_input_witness_outputfirst. ((pfrep_position_aligned_left_input_witness_outputfirst+S (pfrep_power_aligned_left_input_witness_output)=(pfaa_length_aligned_left_input)) /\ ((((exists ff_h_pfp_aligned_left_input_witness_outputfirstentry. ff_h_pfp_aligned_left_input_witness_outputfirstentry + S (pfrep_left_aligned_left_input_witness_output) = S ((S (pfrep_position_aligned_left_input_witness_outputfirst)) * pfaa_sum_c_aligned_left_input)) /\ exists ff_q_pfp_aligned_left_input_witness_outputfirstentry. pfaa_sum_b_aligned_left_input = ff_q_pfp_aligned_left_input_witness_outputfirstentry * S ((S (pfrep_position_aligned_left_input_witness_outputfirst)) * pfaa_sum_c_aligned_left_input) + (pfrep_left_aligned_left_input_witness_output)))))) \/ (((exists pfrep_gap_aligned_left_input_witness_outputfirstoutside. pfrep_gap_aligned_left_input_witness_outputfirstoutside+(pfaa_length_aligned_left_input)=(pfrep_power_aligned_left_input_witness_output)) /\ (((pfrep_left_aligned_left_input_witness_output)=0))))) -> ((exists pfrep_position_aligned_left_input_witness_outputsecond. ((pfrep_position_aligned_left_input_witness_outputsecond+S (pfrep_power_aligned_left_input_witness_output)=(N)) /\ ((((exists ff_h_pfp_aligned_left_input_witness_outputsecondentry. ff_h_pfp_aligned_left_input_witness_outputsecondentry + S (pfrep_right_aligned_left_input_witness_output) = S ((S (pfrep_position_aligned_left_input_witness_outputsecond)) * wc)) /\ exists ff_q_pfp_aligned_left_input_witness_outputsecondentry. wb = ff_q_pfp_aligned_left_input_witness_outputsecondentry * S ((S (pfrep_position_aligned_left_input_witness_outputsecond)) * wc) + (pfrep_right_aligned_left_input_witness_output)))))) \/ (((exists pfrep_gap_aligned_left_input_witness_outputsecondoutside. pfrep_gap_aligned_left_input_witness_outputsecondoutside+(N)=(pfrep_power_aligned_left_input_witness_output)) /\ (((pfrep_right_aligned_left_input_witness_output)=0))))) -> pfrep_left_aligned_left_input_witness_output=pfrep_right_aligned_left_input_witness_output))))))))))))) -> (((forall fom_index_pfp_aligned_left_pbleft. (exists fom_gap_pfp_aligned_left_pbleft_index_bound. fom_gap_pfp_aligned_left_pbleft_index_bound + S (fom_index_pfp_aligned_left_pbleft) = J) -> exists fom_value_pfp_aligned_left_pbleft. ((((exists fom_beta_height_pfp_aligned_left_pbleft_entry. fom_beta_height_pfp_aligned_left_pbleft_entry + S (fom_value_pfp_aligned_left_pbleft) = S ((S (fom_index_pfp_aligned_left_pbleft)) * dc)) /\ exists fom_beta_quotient_pfp_aligned_left_pbleft_entry. db = fom_beta_quotient_pfp_aligned_left_pbleft_entry * S ((S (fom_index_pfp_aligned_left_pbleft)) * dc) + (fom_value_pfp_aligned_left_pbleft))) /\ (exists fom_gap_pfp_aligned_left_pbleft_value_bound. fom_gap_pfp_aligned_left_pbleft_value_bound + S (fom_value_pfp_aligned_left_pbleft) = p))) /\ (((forall fom_index_pfp_aligned_left_pbright. (exists fom_gap_pfp_aligned_left_pbright_index_bound. fom_gap_pfp_aligned_left_pbright_index_bound + S (fom_index_pfp_aligned_left_pbright) = L) -> exists fom_value_pfp_aligned_left_pbright. ((((exists fom_beta_height_pfp_aligned_left_pbright_entry. fom_beta_height_pfp_aligned_left_pbright_entry + S (fom_value_pfp_aligned_left_pbright) = S ((S (fom_index_pfp_aligned_left_pbright)) * uc)) /\ exists fom_beta_quotient_pfp_aligned_left_pbright_entry. ub = fom_beta_quotient_pfp_aligned_left_pbright_entry * S ((S (fom_index_pfp_aligned_left_pbright)) * uc) + (fom_value_pfp_aligned_left_pbright))) /\ (exists fom_gap_pfp_aligned_left_pbright_value_bound. fom_gap_pfp_aligned_left_pbright_value_bound + S (fom_value_pfp_aligned_left_pbright) = p))) /\ (((((((J)=0 \/ (L)=0) /\ (((H)=0)))) \/ (((~((J)=0)) /\ (((~((L)=0)) /\ (((J)+(L)=S (H)))))))) /\ ((forall pfc_index_aligned_left_pbcoefficients. (exists pfa_gap_aligned_left_pbcoefficientsbound. pfa_gap_aligned_left_pbcoefficientsbound + S (pfc_index_aligned_left_pbcoefficients) = (H)) -> exists pfc_value_aligned_left_pbcoefficients. ((((exists ff_h_pfp_aligned_left_pbcoefficientsentry. ff_h_pfp_aligned_left_pbcoefficientsentry + S (pfc_value_aligned_left_pbcoefficients) = S ((S (pfc_index_aligned_left_pbcoefficients)) * pc)) /\ exists ff_q_pfp_aligned_left_pbcoefficientsentry. pb = ff_q_pfp_aligned_left_pbcoefficientsentry * S ((S (pfc_index_aligned_left_pbcoefficients)) * pc) + (pfc_value_aligned_left_pbcoefficients))) /\ ((exists pfc_terms_code_aligned_left_pbcoefficientscoefficient pfc_terms_scale_aligned_left_pbcoefficientscoefficient pfc_natural_sum_aligned_left_pbcoefficientscoefficient. ((forall pfc_index_aligned_left_pbcoefficientscoefficientdiagonal. (exists pfa_gap_aligned_left_pbcoefficientscoefficientdiagonalbound. pfa_gap_aligned_left_pbcoefficientscoefficientdiagonalbound + S (pfc_index_aligned_left_pbcoefficientscoefficientdiagonal) = (S (pfc_index_aligned_left_pbcoefficients))) -> exists pfc_value_aligned_left_pbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_aligned_left_pbcoefficientscoefficientdiagonalentry. ff_h_pfp_aligned_left_pbcoefficientscoefficientdiagonalentry + S (pfc_value_aligned_left_pbcoefficientscoefficientdiagonal) = S ((S (pfc_index_aligned_left_pbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_left_pbcoefficientscoefficient)) /\ exists ff_q_pfp_aligned_left_pbcoefficientscoefficientdiagonalentry. pfc_terms_code_aligned_left_pbcoefficientscoefficient = ff_q_pfp_aligned_left_pbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_aligned_left_pbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_left_pbcoefficientscoefficient) + (pfc_value_aligned_left_pbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_aligned_left_pbcoefficientscoefficientdiagonalterm pfc_left_aligned_left_pbcoefficientscoefficientdiagonalterm pfc_right_aligned_left_pbcoefficientscoefficientdiagonalterm. (((pfc_index_aligned_left_pbcoefficientscoefficientdiagonal)+pfc_complement_aligned_left_pbcoefficientscoefficientdiagonalterm=(pfc_index_aligned_left_pbcoefficients)) /\ ((((((exists pfa_gap_aligned_left_pbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_aligned_left_pbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_aligned_left_pbcoefficientscoefficientdiagonal) = (J)) /\ ((((exists ff_h_pfp_aligned_left_pbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_aligned_left_pbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_aligned_left_pbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_aligned_left_pbcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_aligned_left_pbcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_aligned_left_pbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_aligned_left_pbcoefficientscoefficientdiagonal)) * dc) + (pfc_left_aligned_left_pbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_left_pbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_aligned_left_pbcoefficientscoefficientdiagonaltermleftoutside+(J)=(pfc_index_aligned_left_pbcoefficientscoefficientdiagonal)) /\ (((pfc_left_aligned_left_pbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_aligned_left_pbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_aligned_left_pbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_aligned_left_pbcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_aligned_left_pbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_aligned_left_pbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_aligned_left_pbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_aligned_left_pbcoefficientscoefficientdiagonalterm)) * uc)) /\ exists ff_q_pfp_aligned_left_pbcoefficientscoefficientdiagonaltermrightentry. ub = ff_q_pfp_aligned_left_pbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_aligned_left_pbcoefficientscoefficientdiagonalterm)) * uc) + (pfc_right_aligned_left_pbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_left_pbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_aligned_left_pbcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_aligned_left_pbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_aligned_left_pbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_aligned_left_pbcoefficientscoefficientdiagonal)=pfc_left_aligned_left_pbcoefficientscoefficientdiagonalterm*pfc_right_aligned_left_pbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_aligned_left_pbcoefficientscoefficientsum fs_v_pfc_aligned_left_pbcoefficientscoefficientsum. ((((exists fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_start. fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_aligned_left_pbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_start. fs_u_pfc_aligned_left_pbcoefficientscoefficientsum = fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_aligned_left_pbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_terminal. fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_aligned_left_pbcoefficientscoefficient) = S ((S (S (pfc_index_aligned_left_pbcoefficients))) * fs_v_pfc_aligned_left_pbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_terminal. fs_u_pfc_aligned_left_pbcoefficientscoefficientsum = fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_aligned_left_pbcoefficients))) * fs_v_pfc_aligned_left_pbcoefficientscoefficientsum) + (pfc_natural_sum_aligned_left_pbcoefficientscoefficient))) /\ forall fs_i_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps = S (pfc_index_aligned_left_pbcoefficients)) -> exists fs_a_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps fs_r_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps fs_s_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_left_pbcoefficientscoefficient)) /\ exists fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_aligned_left_pbcoefficientscoefficient = fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_left_pbcoefficientscoefficient) + (fs_a_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_pbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_aligned_left_pbcoefficientscoefficientsum = fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_pbcoefficientscoefficientsum) + (fs_r_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_pbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_aligned_left_pbcoefficientscoefficientsum = fs_q_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_pbcoefficientscoefficientsum) + (fs_s_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps = fs_r_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps + fs_a_pfc_aligned_left_pbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_aligned_left_pbcoefficientscoefficientresiduebound. pfa_gap_aligned_left_pbcoefficientscoefficientresiduebound + S (pfc_value_aligned_left_pbcoefficients) = (p)) /\ ((exists pfa_offset_left_aligned_left_pbcoefficientscoefficientresiduecongruence pfa_offset_right_aligned_left_pbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_aligned_left_pbcoefficientscoefficient) + (p) * pfa_offset_left_aligned_left_pbcoefficientscoefficientresiduecongruence = (pfc_value_aligned_left_pbcoefficients) + (p) * pfa_offset_right_aligned_left_pbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_aligned_left_qbleft. (exists fom_gap_pfp_aligned_left_qbleft_index_bound. fom_gap_pfp_aligned_left_qbleft_index_bound + S (fom_index_pfp_aligned_left_qbleft) = J) -> exists fom_value_pfp_aligned_left_qbleft. ((((exists fom_beta_height_pfp_aligned_left_qbleft_entry. fom_beta_height_pfp_aligned_left_qbleft_entry + S (fom_value_pfp_aligned_left_qbleft) = S ((S (fom_index_pfp_aligned_left_qbleft)) * dc)) /\ exists fom_beta_quotient_pfp_aligned_left_qbleft_entry. db = fom_beta_quotient_pfp_aligned_left_qbleft_entry * S ((S (fom_index_pfp_aligned_left_qbleft)) * dc) + (fom_value_pfp_aligned_left_qbleft))) /\ (exists fom_gap_pfp_aligned_left_qbleft_value_bound. fom_gap_pfp_aligned_left_qbleft_value_bound + S (fom_value_pfp_aligned_left_qbleft) = p))) /\ (((forall fom_index_pfp_aligned_left_qbright. (exists fom_gap_pfp_aligned_left_qbright_index_bound. fom_gap_pfp_aligned_left_qbright_index_bound + S (fom_index_pfp_aligned_left_qbright) = M) -> exists fom_value_pfp_aligned_left_qbright. ((((exists fom_beta_height_pfp_aligned_left_qbright_entry. fom_beta_height_pfp_aligned_left_qbright_entry + S (fom_value_pfp_aligned_left_qbright) = S ((S (fom_index_pfp_aligned_left_qbright)) * vc)) /\ exists fom_beta_quotient_pfp_aligned_left_qbright_entry. vb = fom_beta_quotient_pfp_aligned_left_qbright_entry * S ((S (fom_index_pfp_aligned_left_qbright)) * vc) + (fom_value_pfp_aligned_left_qbright))) /\ (exists fom_gap_pfp_aligned_left_qbright_value_bound. fom_gap_pfp_aligned_left_qbright_value_bound + S (fom_value_pfp_aligned_left_qbright) = p))) /\ (((((((J)=0 \/ (M)=0) /\ (((I)=0)))) \/ (((~((J)=0)) /\ (((~((M)=0)) /\ (((J)+(M)=S (I)))))))) /\ ((forall pfc_index_aligned_left_qbcoefficients. (exists pfa_gap_aligned_left_qbcoefficientsbound. pfa_gap_aligned_left_qbcoefficientsbound + S (pfc_index_aligned_left_qbcoefficients) = (I)) -> exists pfc_value_aligned_left_qbcoefficients. ((((exists ff_h_pfp_aligned_left_qbcoefficientsentry. ff_h_pfp_aligned_left_qbcoefficientsentry + S (pfc_value_aligned_left_qbcoefficients) = S ((S (pfc_index_aligned_left_qbcoefficients)) * qc)) /\ exists ff_q_pfp_aligned_left_qbcoefficientsentry. qb = ff_q_pfp_aligned_left_qbcoefficientsentry * S ((S (pfc_index_aligned_left_qbcoefficients)) * qc) + (pfc_value_aligned_left_qbcoefficients))) /\ ((exists pfc_terms_code_aligned_left_qbcoefficientscoefficient pfc_terms_scale_aligned_left_qbcoefficientscoefficient pfc_natural_sum_aligned_left_qbcoefficientscoefficient. ((forall pfc_index_aligned_left_qbcoefficientscoefficientdiagonal. (exists pfa_gap_aligned_left_qbcoefficientscoefficientdiagonalbound. pfa_gap_aligned_left_qbcoefficientscoefficientdiagonalbound + S (pfc_index_aligned_left_qbcoefficientscoefficientdiagonal) = (S (pfc_index_aligned_left_qbcoefficients))) -> exists pfc_value_aligned_left_qbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_aligned_left_qbcoefficientscoefficientdiagonalentry. ff_h_pfp_aligned_left_qbcoefficientscoefficientdiagonalentry + S (pfc_value_aligned_left_qbcoefficientscoefficientdiagonal) = S ((S (pfc_index_aligned_left_qbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_left_qbcoefficientscoefficient)) /\ exists ff_q_pfp_aligned_left_qbcoefficientscoefficientdiagonalentry. pfc_terms_code_aligned_left_qbcoefficientscoefficient = ff_q_pfp_aligned_left_qbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_aligned_left_qbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_left_qbcoefficientscoefficient) + (pfc_value_aligned_left_qbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_aligned_left_qbcoefficientscoefficientdiagonalterm pfc_left_aligned_left_qbcoefficientscoefficientdiagonalterm pfc_right_aligned_left_qbcoefficientscoefficientdiagonalterm. (((pfc_index_aligned_left_qbcoefficientscoefficientdiagonal)+pfc_complement_aligned_left_qbcoefficientscoefficientdiagonalterm=(pfc_index_aligned_left_qbcoefficients)) /\ ((((((exists pfa_gap_aligned_left_qbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_aligned_left_qbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_aligned_left_qbcoefficientscoefficientdiagonal) = (J)) /\ ((((exists ff_h_pfp_aligned_left_qbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_aligned_left_qbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_aligned_left_qbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_aligned_left_qbcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_aligned_left_qbcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_aligned_left_qbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_aligned_left_qbcoefficientscoefficientdiagonal)) * dc) + (pfc_left_aligned_left_qbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_left_qbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_aligned_left_qbcoefficientscoefficientdiagonaltermleftoutside+(J)=(pfc_index_aligned_left_qbcoefficientscoefficientdiagonal)) /\ (((pfc_left_aligned_left_qbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_aligned_left_qbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_aligned_left_qbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_aligned_left_qbcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_aligned_left_qbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_aligned_left_qbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_aligned_left_qbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_aligned_left_qbcoefficientscoefficientdiagonalterm)) * vc)) /\ exists ff_q_pfp_aligned_left_qbcoefficientscoefficientdiagonaltermrightentry. vb = ff_q_pfp_aligned_left_qbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_aligned_left_qbcoefficientscoefficientdiagonalterm)) * vc) + (pfc_right_aligned_left_qbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_left_qbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_aligned_left_qbcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_aligned_left_qbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_aligned_left_qbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_aligned_left_qbcoefficientscoefficientdiagonal)=pfc_left_aligned_left_qbcoefficientscoefficientdiagonalterm*pfc_right_aligned_left_qbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_aligned_left_qbcoefficientscoefficientsum fs_v_pfc_aligned_left_qbcoefficientscoefficientsum. ((((exists fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_start. fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_aligned_left_qbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_start. fs_u_pfc_aligned_left_qbcoefficientscoefficientsum = fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_aligned_left_qbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_terminal. fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_aligned_left_qbcoefficientscoefficient) = S ((S (S (pfc_index_aligned_left_qbcoefficients))) * fs_v_pfc_aligned_left_qbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_terminal. fs_u_pfc_aligned_left_qbcoefficientscoefficientsum = fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_aligned_left_qbcoefficients))) * fs_v_pfc_aligned_left_qbcoefficientscoefficientsum) + (pfc_natural_sum_aligned_left_qbcoefficientscoefficient))) /\ forall fs_i_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps = S (pfc_index_aligned_left_qbcoefficients)) -> exists fs_a_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps fs_r_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps fs_s_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_left_qbcoefficientscoefficient)) /\ exists fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_aligned_left_qbcoefficientscoefficient = fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_left_qbcoefficientscoefficient) + (fs_a_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_qbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_aligned_left_qbcoefficientscoefficientsum = fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_qbcoefficientscoefficientsum) + (fs_r_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_qbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_aligned_left_qbcoefficientscoefficientsum = fs_q_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_qbcoefficientscoefficientsum) + (fs_s_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps = fs_r_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps + fs_a_pfc_aligned_left_qbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_aligned_left_qbcoefficientscoefficientresiduebound. pfa_gap_aligned_left_qbcoefficientscoefficientresiduebound + S (pfc_value_aligned_left_qbcoefficients) = (p)) /\ ((exists pfa_offset_left_aligned_left_qbcoefficientscoefficientresiduecongruence pfa_offset_right_aligned_left_qbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_aligned_left_qbcoefficientscoefficient) + (p) * pfa_offset_left_aligned_left_qbcoefficientscoefficientresiduecongruence = (pfc_value_aligned_left_qbcoefficients) + (p) * pfa_offset_right_aligned_left_qbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_aligned_left_rbleft. (exists fom_gap_pfp_aligned_left_rbleft_index_bound. fom_gap_pfp_aligned_left_rbleft_index_bound + S (fom_index_pfp_aligned_left_rbleft) = J) -> exists fom_value_pfp_aligned_left_rbleft. ((((exists fom_beta_height_pfp_aligned_left_rbleft_entry. fom_beta_height_pfp_aligned_left_rbleft_entry + S (fom_value_pfp_aligned_left_rbleft) = S ((S (fom_index_pfp_aligned_left_rbleft)) * dc)) /\ exists fom_beta_quotient_pfp_aligned_left_rbleft_entry. db = fom_beta_quotient_pfp_aligned_left_rbleft_entry * S ((S (fom_index_pfp_aligned_left_rbleft)) * dc) + (fom_value_pfp_aligned_left_rbleft))) /\ (exists fom_gap_pfp_aligned_left_rbleft_value_bound. fom_gap_pfp_aligned_left_rbleft_value_bound + S (fom_value_pfp_aligned_left_rbleft) = p))) /\ (((forall fom_index_pfp_aligned_left_rbright. (exists fom_gap_pfp_aligned_left_rbright_index_bound. fom_gap_pfp_aligned_left_rbright_index_bound + S (fom_index_pfp_aligned_left_rbright) = N) -> exists fom_value_pfp_aligned_left_rbright. ((((exists fom_beta_height_pfp_aligned_left_rbright_entry. fom_beta_height_pfp_aligned_left_rbright_entry + S (fom_value_pfp_aligned_left_rbright) = S ((S (fom_index_pfp_aligned_left_rbright)) * wc)) /\ exists fom_beta_quotient_pfp_aligned_left_rbright_entry. wb = fom_beta_quotient_pfp_aligned_left_rbright_entry * S ((S (fom_index_pfp_aligned_left_rbright)) * wc) + (fom_value_pfp_aligned_left_rbright))) /\ (exists fom_gap_pfp_aligned_left_rbright_value_bound. fom_gap_pfp_aligned_left_rbright_value_bound + S (fom_value_pfp_aligned_left_rbright) = p))) /\ (((((((J)=0 \/ (N)=0) /\ (((K)=0)))) \/ (((~((J)=0)) /\ (((~((N)=0)) /\ (((J)+(N)=S (K)))))))) /\ ((forall pfc_index_aligned_left_rbcoefficients. (exists pfa_gap_aligned_left_rbcoefficientsbound. pfa_gap_aligned_left_rbcoefficientsbound + S (pfc_index_aligned_left_rbcoefficients) = (K)) -> exists pfc_value_aligned_left_rbcoefficients. ((((exists ff_h_pfp_aligned_left_rbcoefficientsentry. ff_h_pfp_aligned_left_rbcoefficientsentry + S (pfc_value_aligned_left_rbcoefficients) = S ((S (pfc_index_aligned_left_rbcoefficients)) * rc)) /\ exists ff_q_pfp_aligned_left_rbcoefficientsentry. rb = ff_q_pfp_aligned_left_rbcoefficientsentry * S ((S (pfc_index_aligned_left_rbcoefficients)) * rc) + (pfc_value_aligned_left_rbcoefficients))) /\ ((exists pfc_terms_code_aligned_left_rbcoefficientscoefficient pfc_terms_scale_aligned_left_rbcoefficientscoefficient pfc_natural_sum_aligned_left_rbcoefficientscoefficient. ((forall pfc_index_aligned_left_rbcoefficientscoefficientdiagonal. (exists pfa_gap_aligned_left_rbcoefficientscoefficientdiagonalbound. pfa_gap_aligned_left_rbcoefficientscoefficientdiagonalbound + S (pfc_index_aligned_left_rbcoefficientscoefficientdiagonal) = (S (pfc_index_aligned_left_rbcoefficients))) -> exists pfc_value_aligned_left_rbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_aligned_left_rbcoefficientscoefficientdiagonalentry. ff_h_pfp_aligned_left_rbcoefficientscoefficientdiagonalentry + S (pfc_value_aligned_left_rbcoefficientscoefficientdiagonal) = S ((S (pfc_index_aligned_left_rbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_left_rbcoefficientscoefficient)) /\ exists ff_q_pfp_aligned_left_rbcoefficientscoefficientdiagonalentry. pfc_terms_code_aligned_left_rbcoefficientscoefficient = ff_q_pfp_aligned_left_rbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_aligned_left_rbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_left_rbcoefficientscoefficient) + (pfc_value_aligned_left_rbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_aligned_left_rbcoefficientscoefficientdiagonalterm pfc_left_aligned_left_rbcoefficientscoefficientdiagonalterm pfc_right_aligned_left_rbcoefficientscoefficientdiagonalterm. (((pfc_index_aligned_left_rbcoefficientscoefficientdiagonal)+pfc_complement_aligned_left_rbcoefficientscoefficientdiagonalterm=(pfc_index_aligned_left_rbcoefficients)) /\ ((((((exists pfa_gap_aligned_left_rbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_aligned_left_rbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_aligned_left_rbcoefficientscoefficientdiagonal) = (J)) /\ ((((exists ff_h_pfp_aligned_left_rbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_aligned_left_rbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_aligned_left_rbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_aligned_left_rbcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_aligned_left_rbcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_aligned_left_rbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_aligned_left_rbcoefficientscoefficientdiagonal)) * dc) + (pfc_left_aligned_left_rbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_left_rbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_aligned_left_rbcoefficientscoefficientdiagonaltermleftoutside+(J)=(pfc_index_aligned_left_rbcoefficientscoefficientdiagonal)) /\ (((pfc_left_aligned_left_rbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_aligned_left_rbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_aligned_left_rbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_aligned_left_rbcoefficientscoefficientdiagonalterm) = (N)) /\ ((((exists ff_h_pfp_aligned_left_rbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_aligned_left_rbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_aligned_left_rbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_aligned_left_rbcoefficientscoefficientdiagonalterm)) * wc)) /\ exists ff_q_pfp_aligned_left_rbcoefficientscoefficientdiagonaltermrightentry. wb = ff_q_pfp_aligned_left_rbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_aligned_left_rbcoefficientscoefficientdiagonalterm)) * wc) + (pfc_right_aligned_left_rbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_left_rbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_aligned_left_rbcoefficientscoefficientdiagonaltermrightoutside+(N)=(pfc_complement_aligned_left_rbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_aligned_left_rbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_aligned_left_rbcoefficientscoefficientdiagonal)=pfc_left_aligned_left_rbcoefficientscoefficientdiagonalterm*pfc_right_aligned_left_rbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_aligned_left_rbcoefficientscoefficientsum fs_v_pfc_aligned_left_rbcoefficientscoefficientsum. ((((exists fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_start. fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_aligned_left_rbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_start. fs_u_pfc_aligned_left_rbcoefficientscoefficientsum = fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_aligned_left_rbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_terminal. fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_aligned_left_rbcoefficientscoefficient) = S ((S (S (pfc_index_aligned_left_rbcoefficients))) * fs_v_pfc_aligned_left_rbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_terminal. fs_u_pfc_aligned_left_rbcoefficientscoefficientsum = fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_aligned_left_rbcoefficients))) * fs_v_pfc_aligned_left_rbcoefficientscoefficientsum) + (pfc_natural_sum_aligned_left_rbcoefficientscoefficient))) /\ forall fs_i_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps = S (pfc_index_aligned_left_rbcoefficients)) -> exists fs_a_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps fs_r_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps fs_s_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_left_rbcoefficientscoefficient)) /\ exists fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_aligned_left_rbcoefficientscoefficient = fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_left_rbcoefficientscoefficient) + (fs_a_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_rbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_aligned_left_rbcoefficientscoefficientsum = fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_rbcoefficientscoefficientsum) + (fs_r_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_rbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_aligned_left_rbcoefficientscoefficientsum = fs_q_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_left_rbcoefficientscoefficientsum) + (fs_s_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps = fs_r_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps + fs_a_pfc_aligned_left_rbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_aligned_left_rbcoefficientscoefficientresiduebound. pfa_gap_aligned_left_rbcoefficientscoefficientresiduebound + S (pfc_value_aligned_left_rbcoefficients) = (p)) /\ ((exists pfa_offset_left_aligned_left_rbcoefficientscoefficientresiduecongruence pfa_offset_right_aligned_left_rbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_aligned_left_rbcoefficientscoefficient) + (p) * pfa_offset_left_aligned_left_rbcoefficientscoefficientresiduecongruence = (pfc_value_aligned_left_rbcoefficients) + (p) * pfa_offset_right_aligned_left_rbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_aligned_left_result_left_bounded. (exists fom_gap_pfp_aligned_left_result_left_bounded_index_bound. fom_gap_pfp_aligned_left_result_left_bounded_index_bound + S (fom_index_pfp_aligned_left_result_left_bounded) = H) -> exists fom_value_pfp_aligned_left_result_left_bounded. ((((exists fom_beta_height_pfp_aligned_left_result_left_bounded_entry. fom_beta_height_pfp_aligned_left_result_left_bounded_entry + S (fom_value_pfp_aligned_left_result_left_bounded) = S ((S (fom_index_pfp_aligned_left_result_left_bounded)) * pc)) /\ exists fom_beta_quotient_pfp_aligned_left_result_left_bounded_entry. pb = fom_beta_quotient_pfp_aligned_left_result_left_bounded_entry * S ((S (fom_index_pfp_aligned_left_result_left_bounded)) * pc) + (fom_value_pfp_aligned_left_result_left_bounded))) /\ (exists fom_gap_pfp_aligned_left_result_left_bounded_value_bound. fom_gap_pfp_aligned_left_result_left_bounded_value_bound + S (fom_value_pfp_aligned_left_result_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_left_result_right_bounded. (exists fom_gap_pfp_aligned_left_result_right_bounded_index_bound. fom_gap_pfp_aligned_left_result_right_bounded_index_bound + S (fom_index_pfp_aligned_left_result_right_bounded) = I) -> exists fom_value_pfp_aligned_left_result_right_bounded. ((((exists fom_beta_height_pfp_aligned_left_result_right_bounded_entry. fom_beta_height_pfp_aligned_left_result_right_bounded_entry + S (fom_value_pfp_aligned_left_result_right_bounded) = S ((S (fom_index_pfp_aligned_left_result_right_bounded)) * qc)) /\ exists fom_beta_quotient_pfp_aligned_left_result_right_bounded_entry. qb = fom_beta_quotient_pfp_aligned_left_result_right_bounded_entry * S ((S (fom_index_pfp_aligned_left_result_right_bounded)) * qc) + (fom_value_pfp_aligned_left_result_right_bounded))) /\ (exists fom_gap_pfp_aligned_left_result_right_bounded_value_bound. fom_gap_pfp_aligned_left_result_right_bounded_value_bound + S (fom_value_pfp_aligned_left_result_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_left_result_result_bounded. (exists fom_gap_pfp_aligned_left_result_result_bounded_index_bound. fom_gap_pfp_aligned_left_result_result_bounded_index_bound + S (fom_index_pfp_aligned_left_result_result_bounded) = K) -> exists fom_value_pfp_aligned_left_result_result_bounded. ((((exists fom_beta_height_pfp_aligned_left_result_result_bounded_entry. fom_beta_height_pfp_aligned_left_result_result_bounded_entry + S (fom_value_pfp_aligned_left_result_result_bounded) = S ((S (fom_index_pfp_aligned_left_result_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_aligned_left_result_result_bounded_entry. rb = fom_beta_quotient_pfp_aligned_left_result_result_bounded_entry * S ((S (fom_index_pfp_aligned_left_result_result_bounded)) * rc) + (fom_value_pfp_aligned_left_result_result_bounded))) /\ (exists fom_gap_pfp_aligned_left_result_result_bounded_value_bound. fom_gap_pfp_aligned_left_result_result_bounded_value_bound + S (fom_value_pfp_aligned_left_result_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_left_result pfaa_left_c_aligned_left_result pfaa_right_b_aligned_left_result pfaa_right_c_aligned_left_result pfaa_sum_b_aligned_left_result pfaa_sum_c_aligned_left_result pfaa_length_aligned_left_result. ((((forall pfrep_power_aligned_left_result_witness_common_left pfrep_left_aligned_left_result_witness_common_left pfrep_right_aligned_left_result_witness_common_left. ((exists pfrep_position_aligned_left_result_witness_common_leftfirst. ((pfrep_position_aligned_left_result_witness_common_leftfirst+S (pfrep_power_aligned_left_result_witness_common_left)=(H)) /\ ((((exists ff_h_pfp_aligned_left_result_witness_common_leftfirstentry. ff_h_pfp_aligned_left_result_witness_common_leftfirstentry + S (pfrep_left_aligned_left_result_witness_common_left) = S ((S (pfrep_position_aligned_left_result_witness_common_leftfirst)) * pc)) /\ exists ff_q_pfp_aligned_left_result_witness_common_leftfirstentry. pb = ff_q_pfp_aligned_left_result_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_left_result_witness_common_leftfirst)) * pc) + (pfrep_left_aligned_left_result_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_left_result_witness_common_leftfirstoutside. pfrep_gap_aligned_left_result_witness_common_leftfirstoutside+(H)=(pfrep_power_aligned_left_result_witness_common_left)) /\ (((pfrep_left_aligned_left_result_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_left_result_witness_common_leftsecond. ((pfrep_position_aligned_left_result_witness_common_leftsecond+S (pfrep_power_aligned_left_result_witness_common_left)=(pfaa_length_aligned_left_result)) /\ ((((exists ff_h_pfp_aligned_left_result_witness_common_leftsecondentry. ff_h_pfp_aligned_left_result_witness_common_leftsecondentry + S (pfrep_right_aligned_left_result_witness_common_left) = S ((S (pfrep_position_aligned_left_result_witness_common_leftsecond)) * pfaa_left_c_aligned_left_result)) /\ exists ff_q_pfp_aligned_left_result_witness_common_leftsecondentry. pfaa_left_b_aligned_left_result = ff_q_pfp_aligned_left_result_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_left_result_witness_common_leftsecond)) * pfaa_left_c_aligned_left_result) + (pfrep_right_aligned_left_result_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_left_result_witness_common_leftsecondoutside. pfrep_gap_aligned_left_result_witness_common_leftsecondoutside+(pfaa_length_aligned_left_result)=(pfrep_power_aligned_left_result_witness_common_left)) /\ (((pfrep_right_aligned_left_result_witness_common_left)=0))))) -> pfrep_left_aligned_left_result_witness_common_left=pfrep_right_aligned_left_result_witness_common_left) /\ ((forall pfrep_power_aligned_left_result_witness_common_right pfrep_left_aligned_left_result_witness_common_right pfrep_right_aligned_left_result_witness_common_right. ((exists pfrep_position_aligned_left_result_witness_common_rightfirst. ((pfrep_position_aligned_left_result_witness_common_rightfirst+S (pfrep_power_aligned_left_result_witness_common_right)=(I)) /\ ((((exists ff_h_pfp_aligned_left_result_witness_common_rightfirstentry. ff_h_pfp_aligned_left_result_witness_common_rightfirstentry + S (pfrep_left_aligned_left_result_witness_common_right) = S ((S (pfrep_position_aligned_left_result_witness_common_rightfirst)) * qc)) /\ exists ff_q_pfp_aligned_left_result_witness_common_rightfirstentry. qb = ff_q_pfp_aligned_left_result_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_left_result_witness_common_rightfirst)) * qc) + (pfrep_left_aligned_left_result_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_left_result_witness_common_rightfirstoutside. pfrep_gap_aligned_left_result_witness_common_rightfirstoutside+(I)=(pfrep_power_aligned_left_result_witness_common_right)) /\ (((pfrep_left_aligned_left_result_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_left_result_witness_common_rightsecond. ((pfrep_position_aligned_left_result_witness_common_rightsecond+S (pfrep_power_aligned_left_result_witness_common_right)=(pfaa_length_aligned_left_result)) /\ ((((exists ff_h_pfp_aligned_left_result_witness_common_rightsecondentry. ff_h_pfp_aligned_left_result_witness_common_rightsecondentry + S (pfrep_right_aligned_left_result_witness_common_right) = S ((S (pfrep_position_aligned_left_result_witness_common_rightsecond)) * pfaa_right_c_aligned_left_result)) /\ exists ff_q_pfp_aligned_left_result_witness_common_rightsecondentry. pfaa_right_b_aligned_left_result = ff_q_pfp_aligned_left_result_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_left_result_witness_common_rightsecond)) * pfaa_right_c_aligned_left_result) + (pfrep_right_aligned_left_result_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_left_result_witness_common_rightsecondoutside. pfrep_gap_aligned_left_result_witness_common_rightsecondoutside+(pfaa_length_aligned_left_result)=(pfrep_power_aligned_left_result_witness_common_right)) /\ (((pfrep_right_aligned_left_result_witness_common_right)=0))))) -> pfrep_left_aligned_left_result_witness_common_right=pfrep_right_aligned_left_result_witness_common_right)))) /\ (((forall pfp_index_aligned_left_result_witness_operation. (exists pfa_gap_aligned_left_result_witness_operationindex. pfa_gap_aligned_left_result_witness_operationindex + S (pfp_index_aligned_left_result_witness_operation) = (pfaa_length_aligned_left_result)) -> exists pfp_left_aligned_left_result_witness_operation pfp_right_aligned_left_result_witness_operation pfp_value_aligned_left_result_witness_operation. ((((exists ff_h_pfp_aligned_left_result_witness_operationleft. ff_h_pfp_aligned_left_result_witness_operationleft + S (pfp_left_aligned_left_result_witness_operation) = S ((S (pfp_index_aligned_left_result_witness_operation)) * pfaa_left_c_aligned_left_result)) /\ exists ff_q_pfp_aligned_left_result_witness_operationleft. pfaa_left_b_aligned_left_result = ff_q_pfp_aligned_left_result_witness_operationleft * S ((S (pfp_index_aligned_left_result_witness_operation)) * pfaa_left_c_aligned_left_result) + (pfp_left_aligned_left_result_witness_operation))) /\ (((((exists ff_h_pfp_aligned_left_result_witness_operationright. ff_h_pfp_aligned_left_result_witness_operationright + S (pfp_right_aligned_left_result_witness_operation) = S ((S (pfp_index_aligned_left_result_witness_operation)) * pfaa_right_c_aligned_left_result)) /\ exists ff_q_pfp_aligned_left_result_witness_operationright. pfaa_right_b_aligned_left_result = ff_q_pfp_aligned_left_result_witness_operationright * S ((S (pfp_index_aligned_left_result_witness_operation)) * pfaa_right_c_aligned_left_result) + (pfp_right_aligned_left_result_witness_operation))) /\ (((((exists ff_h_pfp_aligned_left_result_witness_operationtarget. ff_h_pfp_aligned_left_result_witness_operationtarget + S (pfp_value_aligned_left_result_witness_operation) = S ((S (pfp_index_aligned_left_result_witness_operation)) * pfaa_sum_c_aligned_left_result)) /\ exists ff_q_pfp_aligned_left_result_witness_operationtarget. pfaa_sum_b_aligned_left_result = ff_q_pfp_aligned_left_result_witness_operationtarget * S ((S (pfp_index_aligned_left_result_witness_operation)) * pfaa_sum_c_aligned_left_result) + (pfp_value_aligned_left_result_witness_operation))) /\ ((((exists pfa_gap_aligned_left_result_witness_operationoperationleft. pfa_gap_aligned_left_result_witness_operationoperationleft + S (pfp_left_aligned_left_result_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_left_result_witness_operationoperationright. pfa_gap_aligned_left_result_witness_operationoperationright + S (pfp_right_aligned_left_result_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_left_result_witness_operationoperationresultbound. pfa_gap_aligned_left_result_witness_operationoperationresultbound + S (pfp_value_aligned_left_result_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_left_result_witness_operationoperationresultcongruence pfa_offset_right_aligned_left_result_witness_operationoperationresultcongruence. ((pfp_left_aligned_left_result_witness_operation) + (pfp_right_aligned_left_result_witness_operation)) + (p) * pfa_offset_left_aligned_left_result_witness_operationoperationresultcongruence = (pfp_value_aligned_left_result_witness_operation) + (p) * pfa_offset_right_aligned_left_result_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_left_result_witness_output pfrep_left_aligned_left_result_witness_output pfrep_right_aligned_left_result_witness_output. ((exists pfrep_position_aligned_left_result_witness_outputfirst. ((pfrep_position_aligned_left_result_witness_outputfirst+S (pfrep_power_aligned_left_result_witness_output)=(pfaa_length_aligned_left_result)) /\ ((((exists ff_h_pfp_aligned_left_result_witness_outputfirstentry. ff_h_pfp_aligned_left_result_witness_outputfirstentry + S (pfrep_left_aligned_left_result_witness_output) = S ((S (pfrep_position_aligned_left_result_witness_outputfirst)) * pfaa_sum_c_aligned_left_result)) /\ exists ff_q_pfp_aligned_left_result_witness_outputfirstentry. pfaa_sum_b_aligned_left_result = ff_q_pfp_aligned_left_result_witness_outputfirstentry * S ((S (pfrep_position_aligned_left_result_witness_outputfirst)) * pfaa_sum_c_aligned_left_result) + (pfrep_left_aligned_left_result_witness_output)))))) \/ (((exists pfrep_gap_aligned_left_result_witness_outputfirstoutside. pfrep_gap_aligned_left_result_witness_outputfirstoutside+(pfaa_length_aligned_left_result)=(pfrep_power_aligned_left_result_witness_output)) /\ (((pfrep_left_aligned_left_result_witness_output)=0))))) -> ((exists pfrep_position_aligned_left_result_witness_outputsecond. ((pfrep_position_aligned_left_result_witness_outputsecond+S (pfrep_power_aligned_left_result_witness_output)=(K)) /\ ((((exists ff_h_pfp_aligned_left_result_witness_outputsecondentry. ff_h_pfp_aligned_left_result_witness_outputsecondentry + S (pfrep_right_aligned_left_result_witness_output) = S ((S (pfrep_position_aligned_left_result_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_aligned_left_result_witness_outputsecondentry. rb = ff_q_pfp_aligned_left_result_witness_outputsecondentry * S ((S (pfrep_position_aligned_left_result_witness_outputsecond)) * rc) + (pfrep_right_aligned_left_result_witness_output)))))) \/ (((exists pfrep_gap_aligned_left_result_witness_outputsecondoutside. pfrep_gap_aligned_left_result_witness_outputsecondoutside+(K)=(pfrep_power_aligned_left_result_witness_output)) /\ (((pfrep_right_aligned_left_result_witness_output)=0))))) -> pfrep_left_aligned_left_result_witness_output=pfrep_right_aligned_left_result_witness_output)))))))))))))
Complete tactic proof in conservative notation
All 194 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.