Actual right 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_right_prime pfa_factor_right_aligned_right_prime. (p) = pfa_factor_left_aligned_right_prime * pfa_factor_right_aligned_right_prime -> pfa_factor_left_aligned_right_prime = 1 \/ pfa_factor_right_aligned_right_prime = 1) -> (((forall fom_index_pfp_aligned_right_input_left_bounded. (exists fom_gap_pfp_aligned_right_input_left_bounded_index_bound. fom_gap_pfp_aligned_right_input_left_bounded_index_bound + S (fom_index_pfp_aligned_right_input_left_bounded) = L) -> exists fom_value_pfp_aligned_right_input_left_bounded. ((((exists fom_beta_height_pfp_aligned_right_input_left_bounded_entry. fom_beta_height_pfp_aligned_right_input_left_bounded_entry + S (fom_value_pfp_aligned_right_input_left_bounded) = S ((S (fom_index_pfp_aligned_right_input_left_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_aligned_right_input_left_bounded_entry. ub = fom_beta_quotient_pfp_aligned_right_input_left_bounded_entry * S ((S (fom_index_pfp_aligned_right_input_left_bounded)) * uc) + (fom_value_pfp_aligned_right_input_left_bounded))) /\ (exists fom_gap_pfp_aligned_right_input_left_bounded_value_bound. fom_gap_pfp_aligned_right_input_left_bounded_value_bound + S (fom_value_pfp_aligned_right_input_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_right_input_right_bounded. (exists fom_gap_pfp_aligned_right_input_right_bounded_index_bound. fom_gap_pfp_aligned_right_input_right_bounded_index_bound + S (fom_index_pfp_aligned_right_input_right_bounded) = M) -> exists fom_value_pfp_aligned_right_input_right_bounded. ((((exists fom_beta_height_pfp_aligned_right_input_right_bounded_entry. fom_beta_height_pfp_aligned_right_input_right_bounded_entry + S (fom_value_pfp_aligned_right_input_right_bounded) = S ((S (fom_index_pfp_aligned_right_input_right_bounded)) * vc)) /\ exists fom_beta_quotient_pfp_aligned_right_input_right_bounded_entry. vb = fom_beta_quotient_pfp_aligned_right_input_right_bounded_entry * S ((S (fom_index_pfp_aligned_right_input_right_bounded)) * vc) + (fom_value_pfp_aligned_right_input_right_bounded))) /\ (exists fom_gap_pfp_aligned_right_input_right_bounded_value_bound. fom_gap_pfp_aligned_right_input_right_bounded_value_bound + S (fom_value_pfp_aligned_right_input_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_right_input_result_bounded. (exists fom_gap_pfp_aligned_right_input_result_bounded_index_bound. fom_gap_pfp_aligned_right_input_result_bounded_index_bound + S (fom_index_pfp_aligned_right_input_result_bounded) = N) -> exists fom_value_pfp_aligned_right_input_result_bounded. ((((exists fom_beta_height_pfp_aligned_right_input_result_bounded_entry. fom_beta_height_pfp_aligned_right_input_result_bounded_entry + S (fom_value_pfp_aligned_right_input_result_bounded) = S ((S (fom_index_pfp_aligned_right_input_result_bounded)) * wc)) /\ exists fom_beta_quotient_pfp_aligned_right_input_result_bounded_entry. wb = fom_beta_quotient_pfp_aligned_right_input_result_bounded_entry * S ((S (fom_index_pfp_aligned_right_input_result_bounded)) * wc) + (fom_value_pfp_aligned_right_input_result_bounded))) /\ (exists fom_gap_pfp_aligned_right_input_result_bounded_value_bound. fom_gap_pfp_aligned_right_input_result_bounded_value_bound + S (fom_value_pfp_aligned_right_input_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_right_input pfaa_left_c_aligned_right_input pfaa_right_b_aligned_right_input pfaa_right_c_aligned_right_input pfaa_sum_b_aligned_right_input pfaa_sum_c_aligned_right_input pfaa_length_aligned_right_input. ((((forall pfrep_power_aligned_right_input_witness_common_left pfrep_left_aligned_right_input_witness_common_left pfrep_right_aligned_right_input_witness_common_left. ((exists pfrep_position_aligned_right_input_witness_common_leftfirst. ((pfrep_position_aligned_right_input_witness_common_leftfirst+S (pfrep_power_aligned_right_input_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_aligned_right_input_witness_common_leftfirstentry. ff_h_pfp_aligned_right_input_witness_common_leftfirstentry + S (pfrep_left_aligned_right_input_witness_common_left) = S ((S (pfrep_position_aligned_right_input_witness_common_leftfirst)) * uc)) /\ exists ff_q_pfp_aligned_right_input_witness_common_leftfirstentry. ub = ff_q_pfp_aligned_right_input_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_right_input_witness_common_leftfirst)) * uc) + (pfrep_left_aligned_right_input_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_right_input_witness_common_leftfirstoutside. pfrep_gap_aligned_right_input_witness_common_leftfirstoutside+(L)=(pfrep_power_aligned_right_input_witness_common_left)) /\ (((pfrep_left_aligned_right_input_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_right_input_witness_common_leftsecond. ((pfrep_position_aligned_right_input_witness_common_leftsecond+S (pfrep_power_aligned_right_input_witness_common_left)=(pfaa_length_aligned_right_input)) /\ ((((exists ff_h_pfp_aligned_right_input_witness_common_leftsecondentry. ff_h_pfp_aligned_right_input_witness_common_leftsecondentry + S (pfrep_right_aligned_right_input_witness_common_left) = S ((S (pfrep_position_aligned_right_input_witness_common_leftsecond)) * pfaa_left_c_aligned_right_input)) /\ exists ff_q_pfp_aligned_right_input_witness_common_leftsecondentry. pfaa_left_b_aligned_right_input = ff_q_pfp_aligned_right_input_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_right_input_witness_common_leftsecond)) * pfaa_left_c_aligned_right_input) + (pfrep_right_aligned_right_input_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_right_input_witness_common_leftsecondoutside. pfrep_gap_aligned_right_input_witness_common_leftsecondoutside+(pfaa_length_aligned_right_input)=(pfrep_power_aligned_right_input_witness_common_left)) /\ (((pfrep_right_aligned_right_input_witness_common_left)=0))))) -> pfrep_left_aligned_right_input_witness_common_left=pfrep_right_aligned_right_input_witness_common_left) /\ ((forall pfrep_power_aligned_right_input_witness_common_right pfrep_left_aligned_right_input_witness_common_right pfrep_right_aligned_right_input_witness_common_right. ((exists pfrep_position_aligned_right_input_witness_common_rightfirst. ((pfrep_position_aligned_right_input_witness_common_rightfirst+S (pfrep_power_aligned_right_input_witness_common_right)=(M)) /\ ((((exists ff_h_pfp_aligned_right_input_witness_common_rightfirstentry. ff_h_pfp_aligned_right_input_witness_common_rightfirstentry + S (pfrep_left_aligned_right_input_witness_common_right) = S ((S (pfrep_position_aligned_right_input_witness_common_rightfirst)) * vc)) /\ exists ff_q_pfp_aligned_right_input_witness_common_rightfirstentry. vb = ff_q_pfp_aligned_right_input_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_right_input_witness_common_rightfirst)) * vc) + (pfrep_left_aligned_right_input_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_right_input_witness_common_rightfirstoutside. pfrep_gap_aligned_right_input_witness_common_rightfirstoutside+(M)=(pfrep_power_aligned_right_input_witness_common_right)) /\ (((pfrep_left_aligned_right_input_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_right_input_witness_common_rightsecond. ((pfrep_position_aligned_right_input_witness_common_rightsecond+S (pfrep_power_aligned_right_input_witness_common_right)=(pfaa_length_aligned_right_input)) /\ ((((exists ff_h_pfp_aligned_right_input_witness_common_rightsecondentry. ff_h_pfp_aligned_right_input_witness_common_rightsecondentry + S (pfrep_right_aligned_right_input_witness_common_right) = S ((S (pfrep_position_aligned_right_input_witness_common_rightsecond)) * pfaa_right_c_aligned_right_input)) /\ exists ff_q_pfp_aligned_right_input_witness_common_rightsecondentry. pfaa_right_b_aligned_right_input = ff_q_pfp_aligned_right_input_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_right_input_witness_common_rightsecond)) * pfaa_right_c_aligned_right_input) + (pfrep_right_aligned_right_input_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_right_input_witness_common_rightsecondoutside. pfrep_gap_aligned_right_input_witness_common_rightsecondoutside+(pfaa_length_aligned_right_input)=(pfrep_power_aligned_right_input_witness_common_right)) /\ (((pfrep_right_aligned_right_input_witness_common_right)=0))))) -> pfrep_left_aligned_right_input_witness_common_right=pfrep_right_aligned_right_input_witness_common_right)))) /\ (((forall pfp_index_aligned_right_input_witness_operation. (exists pfa_gap_aligned_right_input_witness_operationindex. pfa_gap_aligned_right_input_witness_operationindex + S (pfp_index_aligned_right_input_witness_operation) = (pfaa_length_aligned_right_input)) -> exists pfp_left_aligned_right_input_witness_operation pfp_right_aligned_right_input_witness_operation pfp_value_aligned_right_input_witness_operation. ((((exists ff_h_pfp_aligned_right_input_witness_operationleft. ff_h_pfp_aligned_right_input_witness_operationleft + S (pfp_left_aligned_right_input_witness_operation) = S ((S (pfp_index_aligned_right_input_witness_operation)) * pfaa_left_c_aligned_right_input)) /\ exists ff_q_pfp_aligned_right_input_witness_operationleft. pfaa_left_b_aligned_right_input = ff_q_pfp_aligned_right_input_witness_operationleft * S ((S (pfp_index_aligned_right_input_witness_operation)) * pfaa_left_c_aligned_right_input) + (pfp_left_aligned_right_input_witness_operation))) /\ (((((exists ff_h_pfp_aligned_right_input_witness_operationright. ff_h_pfp_aligned_right_input_witness_operationright + S (pfp_right_aligned_right_input_witness_operation) = S ((S (pfp_index_aligned_right_input_witness_operation)) * pfaa_right_c_aligned_right_input)) /\ exists ff_q_pfp_aligned_right_input_witness_operationright. pfaa_right_b_aligned_right_input = ff_q_pfp_aligned_right_input_witness_operationright * S ((S (pfp_index_aligned_right_input_witness_operation)) * pfaa_right_c_aligned_right_input) + (pfp_right_aligned_right_input_witness_operation))) /\ (((((exists ff_h_pfp_aligned_right_input_witness_operationtarget. ff_h_pfp_aligned_right_input_witness_operationtarget + S (pfp_value_aligned_right_input_witness_operation) = S ((S (pfp_index_aligned_right_input_witness_operation)) * pfaa_sum_c_aligned_right_input)) /\ exists ff_q_pfp_aligned_right_input_witness_operationtarget. pfaa_sum_b_aligned_right_input = ff_q_pfp_aligned_right_input_witness_operationtarget * S ((S (pfp_index_aligned_right_input_witness_operation)) * pfaa_sum_c_aligned_right_input) + (pfp_value_aligned_right_input_witness_operation))) /\ ((((exists pfa_gap_aligned_right_input_witness_operationoperationleft. pfa_gap_aligned_right_input_witness_operationoperationleft + S (pfp_left_aligned_right_input_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_right_input_witness_operationoperationright. pfa_gap_aligned_right_input_witness_operationoperationright + S (pfp_right_aligned_right_input_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_right_input_witness_operationoperationresultbound. pfa_gap_aligned_right_input_witness_operationoperationresultbound + S (pfp_value_aligned_right_input_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_right_input_witness_operationoperationresultcongruence pfa_offset_right_aligned_right_input_witness_operationoperationresultcongruence. ((pfp_left_aligned_right_input_witness_operation) + (pfp_right_aligned_right_input_witness_operation)) + (p) * pfa_offset_left_aligned_right_input_witness_operationoperationresultcongruence = (pfp_value_aligned_right_input_witness_operation) + (p) * pfa_offset_right_aligned_right_input_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_right_input_witness_output pfrep_left_aligned_right_input_witness_output pfrep_right_aligned_right_input_witness_output. ((exists pfrep_position_aligned_right_input_witness_outputfirst. ((pfrep_position_aligned_right_input_witness_outputfirst+S (pfrep_power_aligned_right_input_witness_output)=(pfaa_length_aligned_right_input)) /\ ((((exists ff_h_pfp_aligned_right_input_witness_outputfirstentry. ff_h_pfp_aligned_right_input_witness_outputfirstentry + S (pfrep_left_aligned_right_input_witness_output) = S ((S (pfrep_position_aligned_right_input_witness_outputfirst)) * pfaa_sum_c_aligned_right_input)) /\ exists ff_q_pfp_aligned_right_input_witness_outputfirstentry. pfaa_sum_b_aligned_right_input = ff_q_pfp_aligned_right_input_witness_outputfirstentry * S ((S (pfrep_position_aligned_right_input_witness_outputfirst)) * pfaa_sum_c_aligned_right_input) + (pfrep_left_aligned_right_input_witness_output)))))) \/ (((exists pfrep_gap_aligned_right_input_witness_outputfirstoutside. pfrep_gap_aligned_right_input_witness_outputfirstoutside+(pfaa_length_aligned_right_input)=(pfrep_power_aligned_right_input_witness_output)) /\ (((pfrep_left_aligned_right_input_witness_output)=0))))) -> ((exists pfrep_position_aligned_right_input_witness_outputsecond. ((pfrep_position_aligned_right_input_witness_outputsecond+S (pfrep_power_aligned_right_input_witness_output)=(N)) /\ ((((exists ff_h_pfp_aligned_right_input_witness_outputsecondentry. ff_h_pfp_aligned_right_input_witness_outputsecondentry + S (pfrep_right_aligned_right_input_witness_output) = S ((S (pfrep_position_aligned_right_input_witness_outputsecond)) * wc)) /\ exists ff_q_pfp_aligned_right_input_witness_outputsecondentry. wb = ff_q_pfp_aligned_right_input_witness_outputsecondentry * S ((S (pfrep_position_aligned_right_input_witness_outputsecond)) * wc) + (pfrep_right_aligned_right_input_witness_output)))))) \/ (((exists pfrep_gap_aligned_right_input_witness_outputsecondoutside. pfrep_gap_aligned_right_input_witness_outputsecondoutside+(N)=(pfrep_power_aligned_right_input_witness_output)) /\ (((pfrep_right_aligned_right_input_witness_output)=0))))) -> pfrep_left_aligned_right_input_witness_output=pfrep_right_aligned_right_input_witness_output))))))))))))) -> (((forall fom_index_pfp_aligned_right_pbleft. (exists fom_gap_pfp_aligned_right_pbleft_index_bound. fom_gap_pfp_aligned_right_pbleft_index_bound + S (fom_index_pfp_aligned_right_pbleft) = L) -> exists fom_value_pfp_aligned_right_pbleft. ((((exists fom_beta_height_pfp_aligned_right_pbleft_entry. fom_beta_height_pfp_aligned_right_pbleft_entry + S (fom_value_pfp_aligned_right_pbleft) = S ((S (fom_index_pfp_aligned_right_pbleft)) * uc)) /\ exists fom_beta_quotient_pfp_aligned_right_pbleft_entry. ub = fom_beta_quotient_pfp_aligned_right_pbleft_entry * S ((S (fom_index_pfp_aligned_right_pbleft)) * uc) + (fom_value_pfp_aligned_right_pbleft))) /\ (exists fom_gap_pfp_aligned_right_pbleft_value_bound. fom_gap_pfp_aligned_right_pbleft_value_bound + S (fom_value_pfp_aligned_right_pbleft) = p))) /\ (((forall fom_index_pfp_aligned_right_pbright. (exists fom_gap_pfp_aligned_right_pbright_index_bound. fom_gap_pfp_aligned_right_pbright_index_bound + S (fom_index_pfp_aligned_right_pbright) = J) -> exists fom_value_pfp_aligned_right_pbright. ((((exists fom_beta_height_pfp_aligned_right_pbright_entry. fom_beta_height_pfp_aligned_right_pbright_entry + S (fom_value_pfp_aligned_right_pbright) = S ((S (fom_index_pfp_aligned_right_pbright)) * dc)) /\ exists fom_beta_quotient_pfp_aligned_right_pbright_entry. db = fom_beta_quotient_pfp_aligned_right_pbright_entry * S ((S (fom_index_pfp_aligned_right_pbright)) * dc) + (fom_value_pfp_aligned_right_pbright))) /\ (exists fom_gap_pfp_aligned_right_pbright_value_bound. fom_gap_pfp_aligned_right_pbright_value_bound + S (fom_value_pfp_aligned_right_pbright) = p))) /\ (((((((L)=0 \/ (J)=0) /\ (((H)=0)))) \/ (((~((L)=0)) /\ (((~((J)=0)) /\ (((L)+(J)=S (H)))))))) /\ ((forall pfc_index_aligned_right_pbcoefficients. (exists pfa_gap_aligned_right_pbcoefficientsbound. pfa_gap_aligned_right_pbcoefficientsbound + S (pfc_index_aligned_right_pbcoefficients) = (H)) -> exists pfc_value_aligned_right_pbcoefficients. ((((exists ff_h_pfp_aligned_right_pbcoefficientsentry. ff_h_pfp_aligned_right_pbcoefficientsentry + S (pfc_value_aligned_right_pbcoefficients) = S ((S (pfc_index_aligned_right_pbcoefficients)) * pc)) /\ exists ff_q_pfp_aligned_right_pbcoefficientsentry. pb = ff_q_pfp_aligned_right_pbcoefficientsentry * S ((S (pfc_index_aligned_right_pbcoefficients)) * pc) + (pfc_value_aligned_right_pbcoefficients))) /\ ((exists pfc_terms_code_aligned_right_pbcoefficientscoefficient pfc_terms_scale_aligned_right_pbcoefficientscoefficient pfc_natural_sum_aligned_right_pbcoefficientscoefficient. ((forall pfc_index_aligned_right_pbcoefficientscoefficientdiagonal. (exists pfa_gap_aligned_right_pbcoefficientscoefficientdiagonalbound. pfa_gap_aligned_right_pbcoefficientscoefficientdiagonalbound + S (pfc_index_aligned_right_pbcoefficientscoefficientdiagonal) = (S (pfc_index_aligned_right_pbcoefficients))) -> exists pfc_value_aligned_right_pbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_aligned_right_pbcoefficientscoefficientdiagonalentry. ff_h_pfp_aligned_right_pbcoefficientscoefficientdiagonalentry + S (pfc_value_aligned_right_pbcoefficientscoefficientdiagonal) = S ((S (pfc_index_aligned_right_pbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_right_pbcoefficientscoefficient)) /\ exists ff_q_pfp_aligned_right_pbcoefficientscoefficientdiagonalentry. pfc_terms_code_aligned_right_pbcoefficientscoefficient = ff_q_pfp_aligned_right_pbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_aligned_right_pbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_right_pbcoefficientscoefficient) + (pfc_value_aligned_right_pbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_aligned_right_pbcoefficientscoefficientdiagonalterm pfc_left_aligned_right_pbcoefficientscoefficientdiagonalterm pfc_right_aligned_right_pbcoefficientscoefficientdiagonalterm. (((pfc_index_aligned_right_pbcoefficientscoefficientdiagonal)+pfc_complement_aligned_right_pbcoefficientscoefficientdiagonalterm=(pfc_index_aligned_right_pbcoefficients)) /\ ((((((exists pfa_gap_aligned_right_pbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_aligned_right_pbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_aligned_right_pbcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_aligned_right_pbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_aligned_right_pbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_aligned_right_pbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_aligned_right_pbcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_aligned_right_pbcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_aligned_right_pbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_aligned_right_pbcoefficientscoefficientdiagonal)) * uc) + (pfc_left_aligned_right_pbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_right_pbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_aligned_right_pbcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_aligned_right_pbcoefficientscoefficientdiagonal)) /\ (((pfc_left_aligned_right_pbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_aligned_right_pbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_aligned_right_pbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_aligned_right_pbcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_aligned_right_pbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_aligned_right_pbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_aligned_right_pbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_aligned_right_pbcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_aligned_right_pbcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_aligned_right_pbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_aligned_right_pbcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_aligned_right_pbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_right_pbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_aligned_right_pbcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_aligned_right_pbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_aligned_right_pbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_aligned_right_pbcoefficientscoefficientdiagonal)=pfc_left_aligned_right_pbcoefficientscoefficientdiagonalterm*pfc_right_aligned_right_pbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_aligned_right_pbcoefficientscoefficientsum fs_v_pfc_aligned_right_pbcoefficientscoefficientsum. ((((exists fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_start. fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_aligned_right_pbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_start. fs_u_pfc_aligned_right_pbcoefficientscoefficientsum = fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_aligned_right_pbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_terminal. fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_aligned_right_pbcoefficientscoefficient) = S ((S (S (pfc_index_aligned_right_pbcoefficients))) * fs_v_pfc_aligned_right_pbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_terminal. fs_u_pfc_aligned_right_pbcoefficientscoefficientsum = fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_aligned_right_pbcoefficients))) * fs_v_pfc_aligned_right_pbcoefficientscoefficientsum) + (pfc_natural_sum_aligned_right_pbcoefficientscoefficient))) /\ forall fs_i_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps = S (pfc_index_aligned_right_pbcoefficients)) -> exists fs_a_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps fs_r_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps fs_s_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_right_pbcoefficientscoefficient)) /\ exists fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_aligned_right_pbcoefficientscoefficient = fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_right_pbcoefficientscoefficient) + (fs_a_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_pbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_aligned_right_pbcoefficientscoefficientsum = fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_pbcoefficientscoefficientsum) + (fs_r_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_pbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_aligned_right_pbcoefficientscoefficientsum = fs_q_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_pbcoefficientscoefficientsum) + (fs_s_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps = fs_r_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps + fs_a_pfc_aligned_right_pbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_aligned_right_pbcoefficientscoefficientresiduebound. pfa_gap_aligned_right_pbcoefficientscoefficientresiduebound + S (pfc_value_aligned_right_pbcoefficients) = (p)) /\ ((exists pfa_offset_left_aligned_right_pbcoefficientscoefficientresiduecongruence pfa_offset_right_aligned_right_pbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_aligned_right_pbcoefficientscoefficient) + (p) * pfa_offset_left_aligned_right_pbcoefficientscoefficientresiduecongruence = (pfc_value_aligned_right_pbcoefficients) + (p) * pfa_offset_right_aligned_right_pbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_aligned_right_qbleft. (exists fom_gap_pfp_aligned_right_qbleft_index_bound. fom_gap_pfp_aligned_right_qbleft_index_bound + S (fom_index_pfp_aligned_right_qbleft) = M) -> exists fom_value_pfp_aligned_right_qbleft. ((((exists fom_beta_height_pfp_aligned_right_qbleft_entry. fom_beta_height_pfp_aligned_right_qbleft_entry + S (fom_value_pfp_aligned_right_qbleft) = S ((S (fom_index_pfp_aligned_right_qbleft)) * vc)) /\ exists fom_beta_quotient_pfp_aligned_right_qbleft_entry. vb = fom_beta_quotient_pfp_aligned_right_qbleft_entry * S ((S (fom_index_pfp_aligned_right_qbleft)) * vc) + (fom_value_pfp_aligned_right_qbleft))) /\ (exists fom_gap_pfp_aligned_right_qbleft_value_bound. fom_gap_pfp_aligned_right_qbleft_value_bound + S (fom_value_pfp_aligned_right_qbleft) = p))) /\ (((forall fom_index_pfp_aligned_right_qbright. (exists fom_gap_pfp_aligned_right_qbright_index_bound. fom_gap_pfp_aligned_right_qbright_index_bound + S (fom_index_pfp_aligned_right_qbright) = J) -> exists fom_value_pfp_aligned_right_qbright. ((((exists fom_beta_height_pfp_aligned_right_qbright_entry. fom_beta_height_pfp_aligned_right_qbright_entry + S (fom_value_pfp_aligned_right_qbright) = S ((S (fom_index_pfp_aligned_right_qbright)) * dc)) /\ exists fom_beta_quotient_pfp_aligned_right_qbright_entry. db = fom_beta_quotient_pfp_aligned_right_qbright_entry * S ((S (fom_index_pfp_aligned_right_qbright)) * dc) + (fom_value_pfp_aligned_right_qbright))) /\ (exists fom_gap_pfp_aligned_right_qbright_value_bound. fom_gap_pfp_aligned_right_qbright_value_bound + S (fom_value_pfp_aligned_right_qbright) = p))) /\ (((((((M)=0 \/ (J)=0) /\ (((I)=0)))) \/ (((~((M)=0)) /\ (((~((J)=0)) /\ (((M)+(J)=S (I)))))))) /\ ((forall pfc_index_aligned_right_qbcoefficients. (exists pfa_gap_aligned_right_qbcoefficientsbound. pfa_gap_aligned_right_qbcoefficientsbound + S (pfc_index_aligned_right_qbcoefficients) = (I)) -> exists pfc_value_aligned_right_qbcoefficients. ((((exists ff_h_pfp_aligned_right_qbcoefficientsentry. ff_h_pfp_aligned_right_qbcoefficientsentry + S (pfc_value_aligned_right_qbcoefficients) = S ((S (pfc_index_aligned_right_qbcoefficients)) * qc)) /\ exists ff_q_pfp_aligned_right_qbcoefficientsentry. qb = ff_q_pfp_aligned_right_qbcoefficientsentry * S ((S (pfc_index_aligned_right_qbcoefficients)) * qc) + (pfc_value_aligned_right_qbcoefficients))) /\ ((exists pfc_terms_code_aligned_right_qbcoefficientscoefficient pfc_terms_scale_aligned_right_qbcoefficientscoefficient pfc_natural_sum_aligned_right_qbcoefficientscoefficient. ((forall pfc_index_aligned_right_qbcoefficientscoefficientdiagonal. (exists pfa_gap_aligned_right_qbcoefficientscoefficientdiagonalbound. pfa_gap_aligned_right_qbcoefficientscoefficientdiagonalbound + S (pfc_index_aligned_right_qbcoefficientscoefficientdiagonal) = (S (pfc_index_aligned_right_qbcoefficients))) -> exists pfc_value_aligned_right_qbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_aligned_right_qbcoefficientscoefficientdiagonalentry. ff_h_pfp_aligned_right_qbcoefficientscoefficientdiagonalentry + S (pfc_value_aligned_right_qbcoefficientscoefficientdiagonal) = S ((S (pfc_index_aligned_right_qbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_right_qbcoefficientscoefficient)) /\ exists ff_q_pfp_aligned_right_qbcoefficientscoefficientdiagonalentry. pfc_terms_code_aligned_right_qbcoefficientscoefficient = ff_q_pfp_aligned_right_qbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_aligned_right_qbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_right_qbcoefficientscoefficient) + (pfc_value_aligned_right_qbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_aligned_right_qbcoefficientscoefficientdiagonalterm pfc_left_aligned_right_qbcoefficientscoefficientdiagonalterm pfc_right_aligned_right_qbcoefficientscoefficientdiagonalterm. (((pfc_index_aligned_right_qbcoefficientscoefficientdiagonal)+pfc_complement_aligned_right_qbcoefficientscoefficientdiagonalterm=(pfc_index_aligned_right_qbcoefficients)) /\ ((((((exists pfa_gap_aligned_right_qbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_aligned_right_qbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_aligned_right_qbcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_aligned_right_qbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_aligned_right_qbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_aligned_right_qbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_aligned_right_qbcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_aligned_right_qbcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_aligned_right_qbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_aligned_right_qbcoefficientscoefficientdiagonal)) * vc) + (pfc_left_aligned_right_qbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_right_qbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_aligned_right_qbcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_aligned_right_qbcoefficientscoefficientdiagonal)) /\ (((pfc_left_aligned_right_qbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_aligned_right_qbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_aligned_right_qbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_aligned_right_qbcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_aligned_right_qbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_aligned_right_qbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_aligned_right_qbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_aligned_right_qbcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_aligned_right_qbcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_aligned_right_qbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_aligned_right_qbcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_aligned_right_qbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_right_qbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_aligned_right_qbcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_aligned_right_qbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_aligned_right_qbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_aligned_right_qbcoefficientscoefficientdiagonal)=pfc_left_aligned_right_qbcoefficientscoefficientdiagonalterm*pfc_right_aligned_right_qbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_aligned_right_qbcoefficientscoefficientsum fs_v_pfc_aligned_right_qbcoefficientscoefficientsum. ((((exists fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_start. fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_aligned_right_qbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_start. fs_u_pfc_aligned_right_qbcoefficientscoefficientsum = fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_aligned_right_qbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_terminal. fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_aligned_right_qbcoefficientscoefficient) = S ((S (S (pfc_index_aligned_right_qbcoefficients))) * fs_v_pfc_aligned_right_qbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_terminal. fs_u_pfc_aligned_right_qbcoefficientscoefficientsum = fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_aligned_right_qbcoefficients))) * fs_v_pfc_aligned_right_qbcoefficientscoefficientsum) + (pfc_natural_sum_aligned_right_qbcoefficientscoefficient))) /\ forall fs_i_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps = S (pfc_index_aligned_right_qbcoefficients)) -> exists fs_a_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps fs_r_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps fs_s_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_right_qbcoefficientscoefficient)) /\ exists fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_aligned_right_qbcoefficientscoefficient = fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_right_qbcoefficientscoefficient) + (fs_a_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_qbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_aligned_right_qbcoefficientscoefficientsum = fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_qbcoefficientscoefficientsum) + (fs_r_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_qbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_aligned_right_qbcoefficientscoefficientsum = fs_q_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_qbcoefficientscoefficientsum) + (fs_s_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps = fs_r_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps + fs_a_pfc_aligned_right_qbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_aligned_right_qbcoefficientscoefficientresiduebound. pfa_gap_aligned_right_qbcoefficientscoefficientresiduebound + S (pfc_value_aligned_right_qbcoefficients) = (p)) /\ ((exists pfa_offset_left_aligned_right_qbcoefficientscoefficientresiduecongruence pfa_offset_right_aligned_right_qbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_aligned_right_qbcoefficientscoefficient) + (p) * pfa_offset_left_aligned_right_qbcoefficientscoefficientresiduecongruence = (pfc_value_aligned_right_qbcoefficients) + (p) * pfa_offset_right_aligned_right_qbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_aligned_right_rbleft. (exists fom_gap_pfp_aligned_right_rbleft_index_bound. fom_gap_pfp_aligned_right_rbleft_index_bound + S (fom_index_pfp_aligned_right_rbleft) = N) -> exists fom_value_pfp_aligned_right_rbleft. ((((exists fom_beta_height_pfp_aligned_right_rbleft_entry. fom_beta_height_pfp_aligned_right_rbleft_entry + S (fom_value_pfp_aligned_right_rbleft) = S ((S (fom_index_pfp_aligned_right_rbleft)) * wc)) /\ exists fom_beta_quotient_pfp_aligned_right_rbleft_entry. wb = fom_beta_quotient_pfp_aligned_right_rbleft_entry * S ((S (fom_index_pfp_aligned_right_rbleft)) * wc) + (fom_value_pfp_aligned_right_rbleft))) /\ (exists fom_gap_pfp_aligned_right_rbleft_value_bound. fom_gap_pfp_aligned_right_rbleft_value_bound + S (fom_value_pfp_aligned_right_rbleft) = p))) /\ (((forall fom_index_pfp_aligned_right_rbright. (exists fom_gap_pfp_aligned_right_rbright_index_bound. fom_gap_pfp_aligned_right_rbright_index_bound + S (fom_index_pfp_aligned_right_rbright) = J) -> exists fom_value_pfp_aligned_right_rbright. ((((exists fom_beta_height_pfp_aligned_right_rbright_entry. fom_beta_height_pfp_aligned_right_rbright_entry + S (fom_value_pfp_aligned_right_rbright) = S ((S (fom_index_pfp_aligned_right_rbright)) * dc)) /\ exists fom_beta_quotient_pfp_aligned_right_rbright_entry. db = fom_beta_quotient_pfp_aligned_right_rbright_entry * S ((S (fom_index_pfp_aligned_right_rbright)) * dc) + (fom_value_pfp_aligned_right_rbright))) /\ (exists fom_gap_pfp_aligned_right_rbright_value_bound. fom_gap_pfp_aligned_right_rbright_value_bound + S (fom_value_pfp_aligned_right_rbright) = p))) /\ (((((((N)=0 \/ (J)=0) /\ (((K)=0)))) \/ (((~((N)=0)) /\ (((~((J)=0)) /\ (((N)+(J)=S (K)))))))) /\ ((forall pfc_index_aligned_right_rbcoefficients. (exists pfa_gap_aligned_right_rbcoefficientsbound. pfa_gap_aligned_right_rbcoefficientsbound + S (pfc_index_aligned_right_rbcoefficients) = (K)) -> exists pfc_value_aligned_right_rbcoefficients. ((((exists ff_h_pfp_aligned_right_rbcoefficientsentry. ff_h_pfp_aligned_right_rbcoefficientsentry + S (pfc_value_aligned_right_rbcoefficients) = S ((S (pfc_index_aligned_right_rbcoefficients)) * rc)) /\ exists ff_q_pfp_aligned_right_rbcoefficientsentry. rb = ff_q_pfp_aligned_right_rbcoefficientsentry * S ((S (pfc_index_aligned_right_rbcoefficients)) * rc) + (pfc_value_aligned_right_rbcoefficients))) /\ ((exists pfc_terms_code_aligned_right_rbcoefficientscoefficient pfc_terms_scale_aligned_right_rbcoefficientscoefficient pfc_natural_sum_aligned_right_rbcoefficientscoefficient. ((forall pfc_index_aligned_right_rbcoefficientscoefficientdiagonal. (exists pfa_gap_aligned_right_rbcoefficientscoefficientdiagonalbound. pfa_gap_aligned_right_rbcoefficientscoefficientdiagonalbound + S (pfc_index_aligned_right_rbcoefficientscoefficientdiagonal) = (S (pfc_index_aligned_right_rbcoefficients))) -> exists pfc_value_aligned_right_rbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_aligned_right_rbcoefficientscoefficientdiagonalentry. ff_h_pfp_aligned_right_rbcoefficientscoefficientdiagonalentry + S (pfc_value_aligned_right_rbcoefficientscoefficientdiagonal) = S ((S (pfc_index_aligned_right_rbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_right_rbcoefficientscoefficient)) /\ exists ff_q_pfp_aligned_right_rbcoefficientscoefficientdiagonalentry. pfc_terms_code_aligned_right_rbcoefficientscoefficient = ff_q_pfp_aligned_right_rbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_aligned_right_rbcoefficientscoefficientdiagonal)) * pfc_terms_scale_aligned_right_rbcoefficientscoefficient) + (pfc_value_aligned_right_rbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_aligned_right_rbcoefficientscoefficientdiagonalterm pfc_left_aligned_right_rbcoefficientscoefficientdiagonalterm pfc_right_aligned_right_rbcoefficientscoefficientdiagonalterm. (((pfc_index_aligned_right_rbcoefficientscoefficientdiagonal)+pfc_complement_aligned_right_rbcoefficientscoefficientdiagonalterm=(pfc_index_aligned_right_rbcoefficients)) /\ ((((((exists pfa_gap_aligned_right_rbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_aligned_right_rbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_aligned_right_rbcoefficientscoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_aligned_right_rbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_aligned_right_rbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_aligned_right_rbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_aligned_right_rbcoefficientscoefficientdiagonal)) * wc)) /\ exists ff_q_pfp_aligned_right_rbcoefficientscoefficientdiagonaltermleftentry. wb = ff_q_pfp_aligned_right_rbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_aligned_right_rbcoefficientscoefficientdiagonal)) * wc) + (pfc_left_aligned_right_rbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_right_rbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_aligned_right_rbcoefficientscoefficientdiagonaltermleftoutside+(N)=(pfc_index_aligned_right_rbcoefficientscoefficientdiagonal)) /\ (((pfc_left_aligned_right_rbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_aligned_right_rbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_aligned_right_rbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_aligned_right_rbcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_aligned_right_rbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_aligned_right_rbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_aligned_right_rbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_aligned_right_rbcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_aligned_right_rbcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_aligned_right_rbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_aligned_right_rbcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_aligned_right_rbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_aligned_right_rbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_aligned_right_rbcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_aligned_right_rbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_aligned_right_rbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_aligned_right_rbcoefficientscoefficientdiagonal)=pfc_left_aligned_right_rbcoefficientscoefficientdiagonalterm*pfc_right_aligned_right_rbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_aligned_right_rbcoefficientscoefficientsum fs_v_pfc_aligned_right_rbcoefficientscoefficientsum. ((((exists fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_start. fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_aligned_right_rbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_start. fs_u_pfc_aligned_right_rbcoefficientscoefficientsum = fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_aligned_right_rbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_terminal. fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_aligned_right_rbcoefficientscoefficient) = S ((S (S (pfc_index_aligned_right_rbcoefficients))) * fs_v_pfc_aligned_right_rbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_terminal. fs_u_pfc_aligned_right_rbcoefficientscoefficientsum = fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_aligned_right_rbcoefficients))) * fs_v_pfc_aligned_right_rbcoefficientscoefficientsum) + (pfc_natural_sum_aligned_right_rbcoefficientscoefficient))) /\ forall fs_i_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps = S (pfc_index_aligned_right_rbcoefficients)) -> exists fs_a_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps fs_r_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps fs_s_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_right_rbcoefficientscoefficient)) /\ exists fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_aligned_right_rbcoefficientscoefficient = fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_aligned_right_rbcoefficientscoefficient) + (fs_a_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_rbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_aligned_right_rbcoefficientscoefficientsum = fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_rbcoefficientscoefficientsum) + (fs_r_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_rbcoefficientscoefficientsum)) /\ exists fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_aligned_right_rbcoefficientscoefficientsum = fs_q_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_aligned_right_rbcoefficientscoefficientsum) + (fs_s_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps = fs_r_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps + fs_a_pfc_aligned_right_rbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_aligned_right_rbcoefficientscoefficientresiduebound. pfa_gap_aligned_right_rbcoefficientscoefficientresiduebound + S (pfc_value_aligned_right_rbcoefficients) = (p)) /\ ((exists pfa_offset_left_aligned_right_rbcoefficientscoefficientresiduecongruence pfa_offset_right_aligned_right_rbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_aligned_right_rbcoefficientscoefficient) + (p) * pfa_offset_left_aligned_right_rbcoefficientscoefficientresiduecongruence = (pfc_value_aligned_right_rbcoefficients) + (p) * pfa_offset_right_aligned_right_rbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_aligned_right_result_left_bounded. (exists fom_gap_pfp_aligned_right_result_left_bounded_index_bound. fom_gap_pfp_aligned_right_result_left_bounded_index_bound + S (fom_index_pfp_aligned_right_result_left_bounded) = H) -> exists fom_value_pfp_aligned_right_result_left_bounded. ((((exists fom_beta_height_pfp_aligned_right_result_left_bounded_entry. fom_beta_height_pfp_aligned_right_result_left_bounded_entry + S (fom_value_pfp_aligned_right_result_left_bounded) = S ((S (fom_index_pfp_aligned_right_result_left_bounded)) * pc)) /\ exists fom_beta_quotient_pfp_aligned_right_result_left_bounded_entry. pb = fom_beta_quotient_pfp_aligned_right_result_left_bounded_entry * S ((S (fom_index_pfp_aligned_right_result_left_bounded)) * pc) + (fom_value_pfp_aligned_right_result_left_bounded))) /\ (exists fom_gap_pfp_aligned_right_result_left_bounded_value_bound. fom_gap_pfp_aligned_right_result_left_bounded_value_bound + S (fom_value_pfp_aligned_right_result_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_right_result_right_bounded. (exists fom_gap_pfp_aligned_right_result_right_bounded_index_bound. fom_gap_pfp_aligned_right_result_right_bounded_index_bound + S (fom_index_pfp_aligned_right_result_right_bounded) = I) -> exists fom_value_pfp_aligned_right_result_right_bounded. ((((exists fom_beta_height_pfp_aligned_right_result_right_bounded_entry. fom_beta_height_pfp_aligned_right_result_right_bounded_entry + S (fom_value_pfp_aligned_right_result_right_bounded) = S ((S (fom_index_pfp_aligned_right_result_right_bounded)) * qc)) /\ exists fom_beta_quotient_pfp_aligned_right_result_right_bounded_entry. qb = fom_beta_quotient_pfp_aligned_right_result_right_bounded_entry * S ((S (fom_index_pfp_aligned_right_result_right_bounded)) * qc) + (fom_value_pfp_aligned_right_result_right_bounded))) /\ (exists fom_gap_pfp_aligned_right_result_right_bounded_value_bound. fom_gap_pfp_aligned_right_result_right_bounded_value_bound + S (fom_value_pfp_aligned_right_result_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_right_result_result_bounded. (exists fom_gap_pfp_aligned_right_result_result_bounded_index_bound. fom_gap_pfp_aligned_right_result_result_bounded_index_bound + S (fom_index_pfp_aligned_right_result_result_bounded) = K) -> exists fom_value_pfp_aligned_right_result_result_bounded. ((((exists fom_beta_height_pfp_aligned_right_result_result_bounded_entry. fom_beta_height_pfp_aligned_right_result_result_bounded_entry + S (fom_value_pfp_aligned_right_result_result_bounded) = S ((S (fom_index_pfp_aligned_right_result_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_aligned_right_result_result_bounded_entry. rb = fom_beta_quotient_pfp_aligned_right_result_result_bounded_entry * S ((S (fom_index_pfp_aligned_right_result_result_bounded)) * rc) + (fom_value_pfp_aligned_right_result_result_bounded))) /\ (exists fom_gap_pfp_aligned_right_result_result_bounded_value_bound. fom_gap_pfp_aligned_right_result_result_bounded_value_bound + S (fom_value_pfp_aligned_right_result_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_right_result pfaa_left_c_aligned_right_result pfaa_right_b_aligned_right_result pfaa_right_c_aligned_right_result pfaa_sum_b_aligned_right_result pfaa_sum_c_aligned_right_result pfaa_length_aligned_right_result. ((((forall pfrep_power_aligned_right_result_witness_common_left pfrep_left_aligned_right_result_witness_common_left pfrep_right_aligned_right_result_witness_common_left. ((exists pfrep_position_aligned_right_result_witness_common_leftfirst. ((pfrep_position_aligned_right_result_witness_common_leftfirst+S (pfrep_power_aligned_right_result_witness_common_left)=(H)) /\ ((((exists ff_h_pfp_aligned_right_result_witness_common_leftfirstentry. ff_h_pfp_aligned_right_result_witness_common_leftfirstentry + S (pfrep_left_aligned_right_result_witness_common_left) = S ((S (pfrep_position_aligned_right_result_witness_common_leftfirst)) * pc)) /\ exists ff_q_pfp_aligned_right_result_witness_common_leftfirstentry. pb = ff_q_pfp_aligned_right_result_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_right_result_witness_common_leftfirst)) * pc) + (pfrep_left_aligned_right_result_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_right_result_witness_common_leftfirstoutside. pfrep_gap_aligned_right_result_witness_common_leftfirstoutside+(H)=(pfrep_power_aligned_right_result_witness_common_left)) /\ (((pfrep_left_aligned_right_result_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_right_result_witness_common_leftsecond. ((pfrep_position_aligned_right_result_witness_common_leftsecond+S (pfrep_power_aligned_right_result_witness_common_left)=(pfaa_length_aligned_right_result)) /\ ((((exists ff_h_pfp_aligned_right_result_witness_common_leftsecondentry. ff_h_pfp_aligned_right_result_witness_common_leftsecondentry + S (pfrep_right_aligned_right_result_witness_common_left) = S ((S (pfrep_position_aligned_right_result_witness_common_leftsecond)) * pfaa_left_c_aligned_right_result)) /\ exists ff_q_pfp_aligned_right_result_witness_common_leftsecondentry. pfaa_left_b_aligned_right_result = ff_q_pfp_aligned_right_result_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_right_result_witness_common_leftsecond)) * pfaa_left_c_aligned_right_result) + (pfrep_right_aligned_right_result_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_right_result_witness_common_leftsecondoutside. pfrep_gap_aligned_right_result_witness_common_leftsecondoutside+(pfaa_length_aligned_right_result)=(pfrep_power_aligned_right_result_witness_common_left)) /\ (((pfrep_right_aligned_right_result_witness_common_left)=0))))) -> pfrep_left_aligned_right_result_witness_common_left=pfrep_right_aligned_right_result_witness_common_left) /\ ((forall pfrep_power_aligned_right_result_witness_common_right pfrep_left_aligned_right_result_witness_common_right pfrep_right_aligned_right_result_witness_common_right. ((exists pfrep_position_aligned_right_result_witness_common_rightfirst. ((pfrep_position_aligned_right_result_witness_common_rightfirst+S (pfrep_power_aligned_right_result_witness_common_right)=(I)) /\ ((((exists ff_h_pfp_aligned_right_result_witness_common_rightfirstentry. ff_h_pfp_aligned_right_result_witness_common_rightfirstentry + S (pfrep_left_aligned_right_result_witness_common_right) = S ((S (pfrep_position_aligned_right_result_witness_common_rightfirst)) * qc)) /\ exists ff_q_pfp_aligned_right_result_witness_common_rightfirstentry. qb = ff_q_pfp_aligned_right_result_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_right_result_witness_common_rightfirst)) * qc) + (pfrep_left_aligned_right_result_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_right_result_witness_common_rightfirstoutside. pfrep_gap_aligned_right_result_witness_common_rightfirstoutside+(I)=(pfrep_power_aligned_right_result_witness_common_right)) /\ (((pfrep_left_aligned_right_result_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_right_result_witness_common_rightsecond. ((pfrep_position_aligned_right_result_witness_common_rightsecond+S (pfrep_power_aligned_right_result_witness_common_right)=(pfaa_length_aligned_right_result)) /\ ((((exists ff_h_pfp_aligned_right_result_witness_common_rightsecondentry. ff_h_pfp_aligned_right_result_witness_common_rightsecondentry + S (pfrep_right_aligned_right_result_witness_common_right) = S ((S (pfrep_position_aligned_right_result_witness_common_rightsecond)) * pfaa_right_c_aligned_right_result)) /\ exists ff_q_pfp_aligned_right_result_witness_common_rightsecondentry. pfaa_right_b_aligned_right_result = ff_q_pfp_aligned_right_result_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_right_result_witness_common_rightsecond)) * pfaa_right_c_aligned_right_result) + (pfrep_right_aligned_right_result_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_right_result_witness_common_rightsecondoutside. pfrep_gap_aligned_right_result_witness_common_rightsecondoutside+(pfaa_length_aligned_right_result)=(pfrep_power_aligned_right_result_witness_common_right)) /\ (((pfrep_right_aligned_right_result_witness_common_right)=0))))) -> pfrep_left_aligned_right_result_witness_common_right=pfrep_right_aligned_right_result_witness_common_right)))) /\ (((forall pfp_index_aligned_right_result_witness_operation. (exists pfa_gap_aligned_right_result_witness_operationindex. pfa_gap_aligned_right_result_witness_operationindex + S (pfp_index_aligned_right_result_witness_operation) = (pfaa_length_aligned_right_result)) -> exists pfp_left_aligned_right_result_witness_operation pfp_right_aligned_right_result_witness_operation pfp_value_aligned_right_result_witness_operation. ((((exists ff_h_pfp_aligned_right_result_witness_operationleft. ff_h_pfp_aligned_right_result_witness_operationleft + S (pfp_left_aligned_right_result_witness_operation) = S ((S (pfp_index_aligned_right_result_witness_operation)) * pfaa_left_c_aligned_right_result)) /\ exists ff_q_pfp_aligned_right_result_witness_operationleft. pfaa_left_b_aligned_right_result = ff_q_pfp_aligned_right_result_witness_operationleft * S ((S (pfp_index_aligned_right_result_witness_operation)) * pfaa_left_c_aligned_right_result) + (pfp_left_aligned_right_result_witness_operation))) /\ (((((exists ff_h_pfp_aligned_right_result_witness_operationright. ff_h_pfp_aligned_right_result_witness_operationright + S (pfp_right_aligned_right_result_witness_operation) = S ((S (pfp_index_aligned_right_result_witness_operation)) * pfaa_right_c_aligned_right_result)) /\ exists ff_q_pfp_aligned_right_result_witness_operationright. pfaa_right_b_aligned_right_result = ff_q_pfp_aligned_right_result_witness_operationright * S ((S (pfp_index_aligned_right_result_witness_operation)) * pfaa_right_c_aligned_right_result) + (pfp_right_aligned_right_result_witness_operation))) /\ (((((exists ff_h_pfp_aligned_right_result_witness_operationtarget. ff_h_pfp_aligned_right_result_witness_operationtarget + S (pfp_value_aligned_right_result_witness_operation) = S ((S (pfp_index_aligned_right_result_witness_operation)) * pfaa_sum_c_aligned_right_result)) /\ exists ff_q_pfp_aligned_right_result_witness_operationtarget. pfaa_sum_b_aligned_right_result = ff_q_pfp_aligned_right_result_witness_operationtarget * S ((S (pfp_index_aligned_right_result_witness_operation)) * pfaa_sum_c_aligned_right_result) + (pfp_value_aligned_right_result_witness_operation))) /\ ((((exists pfa_gap_aligned_right_result_witness_operationoperationleft. pfa_gap_aligned_right_result_witness_operationoperationleft + S (pfp_left_aligned_right_result_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_right_result_witness_operationoperationright. pfa_gap_aligned_right_result_witness_operationoperationright + S (pfp_right_aligned_right_result_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_right_result_witness_operationoperationresultbound. pfa_gap_aligned_right_result_witness_operationoperationresultbound + S (pfp_value_aligned_right_result_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_right_result_witness_operationoperationresultcongruence pfa_offset_right_aligned_right_result_witness_operationoperationresultcongruence. ((pfp_left_aligned_right_result_witness_operation) + (pfp_right_aligned_right_result_witness_operation)) + (p) * pfa_offset_left_aligned_right_result_witness_operationoperationresultcongruence = (pfp_value_aligned_right_result_witness_operation) + (p) * pfa_offset_right_aligned_right_result_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_right_result_witness_output pfrep_left_aligned_right_result_witness_output pfrep_right_aligned_right_result_witness_output. ((exists pfrep_position_aligned_right_result_witness_outputfirst. ((pfrep_position_aligned_right_result_witness_outputfirst+S (pfrep_power_aligned_right_result_witness_output)=(pfaa_length_aligned_right_result)) /\ ((((exists ff_h_pfp_aligned_right_result_witness_outputfirstentry. ff_h_pfp_aligned_right_result_witness_outputfirstentry + S (pfrep_left_aligned_right_result_witness_output) = S ((S (pfrep_position_aligned_right_result_witness_outputfirst)) * pfaa_sum_c_aligned_right_result)) /\ exists ff_q_pfp_aligned_right_result_witness_outputfirstentry. pfaa_sum_b_aligned_right_result = ff_q_pfp_aligned_right_result_witness_outputfirstentry * S ((S (pfrep_position_aligned_right_result_witness_outputfirst)) * pfaa_sum_c_aligned_right_result) + (pfrep_left_aligned_right_result_witness_output)))))) \/ (((exists pfrep_gap_aligned_right_result_witness_outputfirstoutside. pfrep_gap_aligned_right_result_witness_outputfirstoutside+(pfaa_length_aligned_right_result)=(pfrep_power_aligned_right_result_witness_output)) /\ (((pfrep_left_aligned_right_result_witness_output)=0))))) -> ((exists pfrep_position_aligned_right_result_witness_outputsecond. ((pfrep_position_aligned_right_result_witness_outputsecond+S (pfrep_power_aligned_right_result_witness_output)=(K)) /\ ((((exists ff_h_pfp_aligned_right_result_witness_outputsecondentry. ff_h_pfp_aligned_right_result_witness_outputsecondentry + S (pfrep_right_aligned_right_result_witness_output) = S ((S (pfrep_position_aligned_right_result_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_aligned_right_result_witness_outputsecondentry. rb = ff_q_pfp_aligned_right_result_witness_outputsecondentry * S ((S (pfrep_position_aligned_right_result_witness_outputsecond)) * rc) + (pfrep_right_aligned_right_result_witness_output)))))) \/ (((exists pfrep_gap_aligned_right_result_witness_outputsecondoutside. pfrep_gap_aligned_right_result_witness_outputsecondoutside+(K)=(pfrep_power_aligned_right_result_witness_output)) /\ (((pfrep_right_aligned_right_result_witness_output)=0))))) -> pfrep_left_aligned_right_result_witness_output=pfrep_right_aligned_right_result_witness_output)))))))))))))
Complete tactic proof in conservative notation
All 195 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.