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