prime_field_polynomial_aligned_convolution_left_add

Exact expanded first-order arithmetic statement

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)))))))))))))