prime_field_polynomial_add_trim_aligned

forall p pb pc N xb xc ub uc ab ac L t rb rc R. (forall fom_index_pfp_trim_aligned_product_bounded. (exists fom_gap_pfp_trim_aligned_product_bounded_index_bound. fom_gap_pfp_trim_aligned_product_bounded_index_bound + S (fom_index_pfp_trim_aligned_product_bounded) = N) -> exists fom_value_pfp_trim_aligned_product_bounded. ((((exists fom_beta_height_pfp_trim_aligned_product_bounded_entry. fom_beta_height_pfp_trim_aligned_product_bounded_entry + S (fom_value_pfp_trim_aligned_product_bounded) = S ((S (fom_index_pfp_trim_aligned_product_bounded)) * pc)) /\ exists fom_beta_quotient_pfp_trim_aligned_product_bounded_entry. pb = fom_beta_quotient_pfp_trim_aligned_product_bounded_entry * S ((S (fom_index_pfp_trim_aligned_product_bounded)) * pc) + (fom_value_pfp_trim_aligned_product_bounded))) /\ (exists fom_gap_pfp_trim_aligned_product_bounded_value_bound. fom_gap_pfp_trim_aligned_product_bounded_value_bound + S (fom_value_pfp_trim_aligned_product_bounded) = p))) -> (forall pfrep_power_trim_aligned_product pfrep_left_trim_aligned_product pfrep_right_trim_aligned_product. ((exists pfrep_position_trim_aligned_productfirst. ((pfrep_position_trim_aligned_productfirst+S (pfrep_power_trim_aligned_product)=(N)) /\ ((((exists ff_h_pfp_trim_aligned_productfirstentry. ff_h_pfp_trim_aligned_productfirstentry + S (pfrep_left_trim_aligned_product) = S ((S (pfrep_position_trim_aligned_productfirst)) * pc)) /\ exists ff_q_pfp_trim_aligned_productfirstentry. pb = ff_q_pfp_trim_aligned_productfirstentry * S ((S (pfrep_position_trim_aligned_productfirst)) * pc) + (pfrep_left_trim_aligned_product)))))) \/ (((exists pfrep_gap_trim_aligned_productfirstoutside. pfrep_gap_trim_aligned_productfirstoutside+(N)=(pfrep_power_trim_aligned_product)) /\ (((pfrep_left_trim_aligned_product)=0))))) -> ((exists pfrep_position_trim_aligned_productsecond. ((pfrep_position_trim_aligned_productsecond+S (pfrep_power_trim_aligned_product)=(L)) /\ ((((exists ff_h_pfp_trim_aligned_productsecondentry. ff_h_pfp_trim_aligned_productsecondentry + S (pfrep_right_trim_aligned_product) = S ((S (pfrep_position_trim_aligned_productsecond)) * xc)) /\ exists ff_q_pfp_trim_aligned_productsecondentry. xb = ff_q_pfp_trim_aligned_productsecondentry * S ((S (pfrep_position_trim_aligned_productsecond)) * xc) + (pfrep_right_trim_aligned_product)))))) \/ (((exists pfrep_gap_trim_aligned_productsecondoutside. pfrep_gap_trim_aligned_productsecondoutside+(L)=(pfrep_power_trim_aligned_product)) /\ (((pfrep_right_trim_aligned_product)=0))))) -> pfrep_left_trim_aligned_product=pfrep_right_trim_aligned_product) -> (forall pfp_index_trim_aligned_sum. (exists pfa_gap_trim_aligned_sumindex. pfa_gap_trim_aligned_sumindex + S (pfp_index_trim_aligned_sum) = (L)) -> exists pfp_left_trim_aligned_sum pfp_right_trim_aligned_sum pfp_value_trim_aligned_sum. ((((exists ff_h_pfp_trim_aligned_sumleft. ff_h_pfp_trim_aligned_sumleft + S (pfp_left_trim_aligned_sum) = S ((S (pfp_index_trim_aligned_sum)) * xc)) /\ exists ff_q_pfp_trim_aligned_sumleft. xb = ff_q_pfp_trim_aligned_sumleft * S ((S (pfp_index_trim_aligned_sum)) * xc) + (pfp_left_trim_aligned_sum))) /\ (((((exists ff_h_pfp_trim_aligned_sumright. ff_h_pfp_trim_aligned_sumright + S (pfp_right_trim_aligned_sum) = S ((S (pfp_index_trim_aligned_sum)) * uc)) /\ exists ff_q_pfp_trim_aligned_sumright. ub = ff_q_pfp_trim_aligned_sumright * S ((S (pfp_index_trim_aligned_sum)) * uc) + (pfp_right_trim_aligned_sum))) /\ (((((exists ff_h_pfp_trim_aligned_sumtarget. ff_h_pfp_trim_aligned_sumtarget + S (pfp_value_trim_aligned_sum) = S ((S (pfp_index_trim_aligned_sum)) * ac)) /\ exists ff_q_pfp_trim_aligned_sumtarget. ab = ff_q_pfp_trim_aligned_sumtarget * S ((S (pfp_index_trim_aligned_sum)) * ac) + (pfp_value_trim_aligned_sum))) /\ ((((exists pfa_gap_trim_aligned_sumoperationleft. pfa_gap_trim_aligned_sumoperationleft + S (pfp_left_trim_aligned_sum) = (p)) /\ (((exists pfa_gap_trim_aligned_sumoperationright. pfa_gap_trim_aligned_sumoperationright + S (pfp_right_trim_aligned_sum) = (p)) /\ ((((exists pfa_gap_trim_aligned_sumoperationresultbound. pfa_gap_trim_aligned_sumoperationresultbound + S (pfp_value_trim_aligned_sum) = (p)) /\ ((exists pfa_offset_left_trim_aligned_sumoperationresultcongruence pfa_offset_right_trim_aligned_sumoperationresultcongruence. ((pfp_left_trim_aligned_sum) + (pfp_right_trim_aligned_sum)) + (p) * pfa_offset_left_trim_aligned_sumoperationresultcongruence = (pfp_value_trim_aligned_sum) + (p) * pfa_offset_right_trim_aligned_sumoperationresultcongruence)))))))))))))))) -> ((((L)=(t)+(R)) /\ (((forall fom_index_pfp_trim_aligned_triminput. (exists fom_gap_pfp_trim_aligned_triminput_index_bound. fom_gap_pfp_trim_aligned_triminput_index_bound + S (fom_index_pfp_trim_aligned_triminput) = L) -> exists fom_value_pfp_trim_aligned_triminput. ((((exists fom_beta_height_pfp_trim_aligned_triminput_entry. fom_beta_height_pfp_trim_aligned_triminput_entry + S (fom_value_pfp_trim_aligned_triminput) = S ((S (fom_index_pfp_trim_aligned_triminput)) * uc)) /\ exists fom_beta_quotient_pfp_trim_aligned_triminput_entry. ub = fom_beta_quotient_pfp_trim_aligned_triminput_entry * S ((S (fom_index_pfp_trim_aligned_triminput)) * uc) + (fom_value_pfp_trim_aligned_triminput))) /\ (exists fom_gap_pfp_trim_aligned_triminput_value_bound. fom_gap_pfp_trim_aligned_triminput_value_bound + S (fom_value_pfp_trim_aligned_triminput) = p))) /\ (((forall pfp_repeat_index_trim_aligned_trimremoved. (exists pfa_gap_trim_aligned_trimremovedindex. pfa_gap_trim_aligned_trimremovedindex + S (pfp_repeat_index_trim_aligned_trimremoved) = (t)) -> (((exists ff_h_pfp_trim_aligned_trimremovedentry. ff_h_pfp_trim_aligned_trimremovedentry + S (0) = S ((S (pfp_repeat_index_trim_aligned_trimremoved)) * uc)) /\ exists ff_q_pfp_trim_aligned_trimremovedentry. ub = ff_q_pfp_trim_aligned_trimremovedentry * S ((S (pfp_repeat_index_trim_aligned_trimremoved)) * uc) + (0)))) /\ (((forall pftrim_index_trim_aligned_trimsuffix pftrim_value_trim_aligned_trimsuffix. (exists pfa_gap_trim_aligned_trimsuffixbound. pfa_gap_trim_aligned_trimsuffixbound + S (pftrim_index_trim_aligned_trimsuffix) = (R)) -> (((exists ff_h_pfp_trim_aligned_trimsuffixsource. ff_h_pfp_trim_aligned_trimsuffixsource + S (pftrim_value_trim_aligned_trimsuffix) = S ((S ((t)+pftrim_index_trim_aligned_trimsuffix)) * uc)) /\ exists ff_q_pfp_trim_aligned_trimsuffixsource. ub = ff_q_pfp_trim_aligned_trimsuffixsource * S ((S ((t)+pftrim_index_trim_aligned_trimsuffix)) * uc) + (pftrim_value_trim_aligned_trimsuffix))) -> (((exists ff_h_pfp_trim_aligned_trimsuffixoutput. ff_h_pfp_trim_aligned_trimsuffixoutput + S (pftrim_value_trim_aligned_trimsuffix) = S ((S (pftrim_index_trim_aligned_trimsuffix)) * rc)) /\ exists ff_q_pfp_trim_aligned_trimsuffixoutput. rb = ff_q_pfp_trim_aligned_trimsuffixoutput * S ((S (pftrim_index_trim_aligned_trimsuffix)) * rc) + (pftrim_value_trim_aligned_trimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_trim_aligned_trimnormal. ((((exists ff_h_pfp_trim_aligned_trimnormalentry. ff_h_pfp_trim_aligned_trimnormalentry + S (pftrim_leading_trim_aligned_trimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_trim_aligned_trimnormalentry. rb = ff_q_pfp_trim_aligned_trimnormalentry * S ((S (0)) * rc) + (pftrim_leading_trim_aligned_trimnormal))) /\ ((~(pftrim_leading_trim_aligned_trimnormal=0))))))))))))))) -> (((forall fom_index_pfp_trim_aligned_result_left_bounded. (exists fom_gap_pfp_trim_aligned_result_left_bounded_index_bound. fom_gap_pfp_trim_aligned_result_left_bounded_index_bound + S (fom_index_pfp_trim_aligned_result_left_bounded) = N) -> exists fom_value_pfp_trim_aligned_result_left_bounded. ((((exists fom_beta_height_pfp_trim_aligned_result_left_bounded_entry. fom_beta_height_pfp_trim_aligned_result_left_bounded_entry + S (fom_value_pfp_trim_aligned_result_left_bounded) = S ((S (fom_index_pfp_trim_aligned_result_left_bounded)) * pc)) /\ exists fom_beta_quotient_pfp_trim_aligned_result_left_bounded_entry. pb = fom_beta_quotient_pfp_trim_aligned_result_left_bounded_entry * S ((S (fom_index_pfp_trim_aligned_result_left_bounded)) * pc) + (fom_value_pfp_trim_aligned_result_left_bounded))) /\ (exists fom_gap_pfp_trim_aligned_result_left_bounded_value_bound. fom_gap_pfp_trim_aligned_result_left_bounded_value_bound + S (fom_value_pfp_trim_aligned_result_left_bounded) = p))) /\ (((forall fom_index_pfp_trim_aligned_result_right_bounded. (exists fom_gap_pfp_trim_aligned_result_right_bounded_index_bound. fom_gap_pfp_trim_aligned_result_right_bounded_index_bound + S (fom_index_pfp_trim_aligned_result_right_bounded) = R) -> exists fom_value_pfp_trim_aligned_result_right_bounded. ((((exists fom_beta_height_pfp_trim_aligned_result_right_bounded_entry. fom_beta_height_pfp_trim_aligned_result_right_bounded_entry + S (fom_value_pfp_trim_aligned_result_right_bounded) = S ((S (fom_index_pfp_trim_aligned_result_right_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_trim_aligned_result_right_bounded_entry. rb = fom_beta_quotient_pfp_trim_aligned_result_right_bounded_entry * S ((S (fom_index_pfp_trim_aligned_result_right_bounded)) * rc) + (fom_value_pfp_trim_aligned_result_right_bounded))) /\ (exists fom_gap_pfp_trim_aligned_result_right_bounded_value_bound. fom_gap_pfp_trim_aligned_result_right_bounded_value_bound + S (fom_value_pfp_trim_aligned_result_right_bounded) = p))) /\ (((forall fom_index_pfp_trim_aligned_result_result_bounded. (exists fom_gap_pfp_trim_aligned_result_result_bounded_index_bound. fom_gap_pfp_trim_aligned_result_result_bounded_index_bound + S (fom_index_pfp_trim_aligned_result_result_bounded) = L) -> exists fom_value_pfp_trim_aligned_result_result_bounded. ((((exists fom_beta_height_pfp_trim_aligned_result_result_bounded_entry. fom_beta_height_pfp_trim_aligned_result_result_bounded_entry + S (fom_value_pfp_trim_aligned_result_result_bounded) = S ((S (fom_index_pfp_trim_aligned_result_result_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_trim_aligned_result_result_bounded_entry. ab = fom_beta_quotient_pfp_trim_aligned_result_result_bounded_entry * S ((S (fom_index_pfp_trim_aligned_result_result_bounded)) * ac) + (fom_value_pfp_trim_aligned_result_result_bounded))) /\ (exists fom_gap_pfp_trim_aligned_result_result_bounded_value_bound. fom_gap_pfp_trim_aligned_result_result_bounded_value_bound + S (fom_value_pfp_trim_aligned_result_result_bounded) = p))) /\ ((exists pfaa_left_b_trim_aligned_result pfaa_left_c_trim_aligned_result pfaa_right_b_trim_aligned_result pfaa_right_c_trim_aligned_result pfaa_sum_b_trim_aligned_result pfaa_sum_c_trim_aligned_result pfaa_length_trim_aligned_result. ((((forall pfrep_power_trim_aligned_result_witness_common_left pfrep_left_trim_aligned_result_witness_common_left pfrep_right_trim_aligned_result_witness_common_left. ((exists pfrep_position_trim_aligned_result_witness_common_leftfirst. ((pfrep_position_trim_aligned_result_witness_common_leftfirst+S (pfrep_power_trim_aligned_result_witness_common_left)=(N)) /\ ((((exists ff_h_pfp_trim_aligned_result_witness_common_leftfirstentry. ff_h_pfp_trim_aligned_result_witness_common_leftfirstentry + S (pfrep_left_trim_aligned_result_witness_common_left) = S ((S (pfrep_position_trim_aligned_result_witness_common_leftfirst)) * pc)) /\ exists ff_q_pfp_trim_aligned_result_witness_common_leftfirstentry. pb = ff_q_pfp_trim_aligned_result_witness_common_leftfirstentry * S ((S (pfrep_position_trim_aligned_result_witness_common_leftfirst)) * pc) + (pfrep_left_trim_aligned_result_witness_common_left)))))) \/ (((exists pfrep_gap_trim_aligned_result_witness_common_leftfirstoutside. pfrep_gap_trim_aligned_result_witness_common_leftfirstoutside+(N)=(pfrep_power_trim_aligned_result_witness_common_left)) /\ (((pfrep_left_trim_aligned_result_witness_common_left)=0))))) -> ((exists pfrep_position_trim_aligned_result_witness_common_leftsecond. ((pfrep_position_trim_aligned_result_witness_common_leftsecond+S (pfrep_power_trim_aligned_result_witness_common_left)=(pfaa_length_trim_aligned_result)) /\ ((((exists ff_h_pfp_trim_aligned_result_witness_common_leftsecondentry. ff_h_pfp_trim_aligned_result_witness_common_leftsecondentry + S (pfrep_right_trim_aligned_result_witness_common_left) = S ((S (pfrep_position_trim_aligned_result_witness_common_leftsecond)) * pfaa_left_c_trim_aligned_result)) /\ exists ff_q_pfp_trim_aligned_result_witness_common_leftsecondentry. pfaa_left_b_trim_aligned_result = ff_q_pfp_trim_aligned_result_witness_common_leftsecondentry * S ((S (pfrep_position_trim_aligned_result_witness_common_leftsecond)) * pfaa_left_c_trim_aligned_result) + (pfrep_right_trim_aligned_result_witness_common_left)))))) \/ (((exists pfrep_gap_trim_aligned_result_witness_common_leftsecondoutside. pfrep_gap_trim_aligned_result_witness_common_leftsecondoutside+(pfaa_length_trim_aligned_result)=(pfrep_power_trim_aligned_result_witness_common_left)) /\ (((pfrep_right_trim_aligned_result_witness_common_left)=0))))) -> pfrep_left_trim_aligned_result_witness_common_left=pfrep_right_trim_aligned_result_witness_common_left) /\ ((forall pfrep_power_trim_aligned_result_witness_common_right pfrep_left_trim_aligned_result_witness_common_right pfrep_right_trim_aligned_result_witness_common_right. ((exists pfrep_position_trim_aligned_result_witness_common_rightfirst. ((pfrep_position_trim_aligned_result_witness_common_rightfirst+S (pfrep_power_trim_aligned_result_witness_common_right)=(R)) /\ ((((exists ff_h_pfp_trim_aligned_result_witness_common_rightfirstentry. ff_h_pfp_trim_aligned_result_witness_common_rightfirstentry + S (pfrep_left_trim_aligned_result_witness_common_right) = S ((S (pfrep_position_trim_aligned_result_witness_common_rightfirst)) * rc)) /\ exists ff_q_pfp_trim_aligned_result_witness_common_rightfirstentry. rb = ff_q_pfp_trim_aligned_result_witness_common_rightfirstentry * S ((S (pfrep_position_trim_aligned_result_witness_common_rightfirst)) * rc) + (pfrep_left_trim_aligned_result_witness_common_right)))))) \/ (((exists pfrep_gap_trim_aligned_result_witness_common_rightfirstoutside. pfrep_gap_trim_aligned_result_witness_common_rightfirstoutside+(R)=(pfrep_power_trim_aligned_result_witness_common_right)) /\ (((pfrep_left_trim_aligned_result_witness_common_right)=0))))) -> ((exists pfrep_position_trim_aligned_result_witness_common_rightsecond. ((pfrep_position_trim_aligned_result_witness_common_rightsecond+S (pfrep_power_trim_aligned_result_witness_common_right)=(pfaa_length_trim_aligned_result)) /\ ((((exists ff_h_pfp_trim_aligned_result_witness_common_rightsecondentry. ff_h_pfp_trim_aligned_result_witness_common_rightsecondentry + S (pfrep_right_trim_aligned_result_witness_common_right) = S ((S (pfrep_position_trim_aligned_result_witness_common_rightsecond)) * pfaa_right_c_trim_aligned_result)) /\ exists ff_q_pfp_trim_aligned_result_witness_common_rightsecondentry. pfaa_right_b_trim_aligned_result = ff_q_pfp_trim_aligned_result_witness_common_rightsecondentry * S ((S (pfrep_position_trim_aligned_result_witness_common_rightsecond)) * pfaa_right_c_trim_aligned_result) + (pfrep_right_trim_aligned_result_witness_common_right)))))) \/ (((exists pfrep_gap_trim_aligned_result_witness_common_rightsecondoutside. pfrep_gap_trim_aligned_result_witness_common_rightsecondoutside+(pfaa_length_trim_aligned_result)=(pfrep_power_trim_aligned_result_witness_common_right)) /\ (((pfrep_right_trim_aligned_result_witness_common_right)=0))))) -> pfrep_left_trim_aligned_result_witness_common_right=pfrep_right_trim_aligned_result_witness_common_right)))) /\ (((forall pfp_index_trim_aligned_result_witness_operation. (exists pfa_gap_trim_aligned_result_witness_operationindex. pfa_gap_trim_aligned_result_witness_operationindex + S (pfp_index_trim_aligned_result_witness_operation) = (pfaa_length_trim_aligned_result)) -> exists pfp_left_trim_aligned_result_witness_operation pfp_right_trim_aligned_result_witness_operation pfp_value_trim_aligned_result_witness_operation. ((((exists ff_h_pfp_trim_aligned_result_witness_operationleft. ff_h_pfp_trim_aligned_result_witness_operationleft + S (pfp_left_trim_aligned_result_witness_operation) = S ((S (pfp_index_trim_aligned_result_witness_operation)) * pfaa_left_c_trim_aligned_result)) /\ exists ff_q_pfp_trim_aligned_result_witness_operationleft. pfaa_left_b_trim_aligned_result = ff_q_pfp_trim_aligned_result_witness_operationleft * S ((S (pfp_index_trim_aligned_result_witness_operation)) * pfaa_left_c_trim_aligned_result) + (pfp_left_trim_aligned_result_witness_operation))) /\ (((((exists ff_h_pfp_trim_aligned_result_witness_operationright. ff_h_pfp_trim_aligned_result_witness_operationright + S (pfp_right_trim_aligned_result_witness_operation) = S ((S (pfp_index_trim_aligned_result_witness_operation)) * pfaa_right_c_trim_aligned_result)) /\ exists ff_q_pfp_trim_aligned_result_witness_operationright. pfaa_right_b_trim_aligned_result = ff_q_pfp_trim_aligned_result_witness_operationright * S ((S (pfp_index_trim_aligned_result_witness_operation)) * pfaa_right_c_trim_aligned_result) + (pfp_right_trim_aligned_result_witness_operation))) /\ (((((exists ff_h_pfp_trim_aligned_result_witness_operationtarget. ff_h_pfp_trim_aligned_result_witness_operationtarget + S (pfp_value_trim_aligned_result_witness_operation) = S ((S (pfp_index_trim_aligned_result_witness_operation)) * pfaa_sum_c_trim_aligned_result)) /\ exists ff_q_pfp_trim_aligned_result_witness_operationtarget. pfaa_sum_b_trim_aligned_result = ff_q_pfp_trim_aligned_result_witness_operationtarget * S ((S (pfp_index_trim_aligned_result_witness_operation)) * pfaa_sum_c_trim_aligned_result) + (pfp_value_trim_aligned_result_witness_operation))) /\ ((((exists pfa_gap_trim_aligned_result_witness_operationoperationleft. pfa_gap_trim_aligned_result_witness_operationoperationleft + S (pfp_left_trim_aligned_result_witness_operation) = (p)) /\ (((exists pfa_gap_trim_aligned_result_witness_operationoperationright. pfa_gap_trim_aligned_result_witness_operationoperationright + S (pfp_right_trim_aligned_result_witness_operation) = (p)) /\ ((((exists pfa_gap_trim_aligned_result_witness_operationoperationresultbound. pfa_gap_trim_aligned_result_witness_operationoperationresultbound + S (pfp_value_trim_aligned_result_witness_operation) = (p)) /\ ((exists pfa_offset_left_trim_aligned_result_witness_operationoperationresultcongruence pfa_offset_right_trim_aligned_result_witness_operationoperationresultcongruence. ((pfp_left_trim_aligned_result_witness_operation) + (pfp_right_trim_aligned_result_witness_operation)) + (p) * pfa_offset_left_trim_aligned_result_witness_operationoperationresultcongruence = (pfp_value_trim_aligned_result_witness_operation) + (p) * pfa_offset_right_trim_aligned_result_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_trim_aligned_result_witness_output pfrep_left_trim_aligned_result_witness_output pfrep_right_trim_aligned_result_witness_output. ((exists pfrep_position_trim_aligned_result_witness_outputfirst. ((pfrep_position_trim_aligned_result_witness_outputfirst+S (pfrep_power_trim_aligned_result_witness_output)=(pfaa_length_trim_aligned_result)) /\ ((((exists ff_h_pfp_trim_aligned_result_witness_outputfirstentry. ff_h_pfp_trim_aligned_result_witness_outputfirstentry + S (pfrep_left_trim_aligned_result_witness_output) = S ((S (pfrep_position_trim_aligned_result_witness_outputfirst)) * pfaa_sum_c_trim_aligned_result)) /\ exists ff_q_pfp_trim_aligned_result_witness_outputfirstentry. pfaa_sum_b_trim_aligned_result = ff_q_pfp_trim_aligned_result_witness_outputfirstentry * S ((S (pfrep_position_trim_aligned_result_witness_outputfirst)) * pfaa_sum_c_trim_aligned_result) + (pfrep_left_trim_aligned_result_witness_output)))))) \/ (((exists pfrep_gap_trim_aligned_result_witness_outputfirstoutside. pfrep_gap_trim_aligned_result_witness_outputfirstoutside+(pfaa_length_trim_aligned_result)=(pfrep_power_trim_aligned_result_witness_output)) /\ (((pfrep_left_trim_aligned_result_witness_output)=0))))) -> ((exists pfrep_position_trim_aligned_result_witness_outputsecond. ((pfrep_position_trim_aligned_result_witness_outputsecond+S (pfrep_power_trim_aligned_result_witness_output)=(L)) /\ ((((exists ff_h_pfp_trim_aligned_result_witness_outputsecondentry. ff_h_pfp_trim_aligned_result_witness_outputsecondentry + S (pfrep_right_trim_aligned_result_witness_output) = S ((S (pfrep_position_trim_aligned_result_witness_outputsecond)) * ac)) /\ exists ff_q_pfp_trim_aligned_result_witness_outputsecondentry. ab = ff_q_pfp_trim_aligned_result_witness_outputsecondentry * S ((S (pfrep_position_trim_aligned_result_witness_outputsecond)) * ac) + (pfrep_right_trim_aligned_result_witness_output)))))) \/ (((exists pfrep_gap_trim_aligned_result_witness_outputsecondoutside. pfrep_gap_trim_aligned_result_witness_outputsecondoutside+(L)=(pfrep_power_trim_aligned_result_witness_output)) /\ (((pfrep_right_trim_aligned_result_witness_output)=0))))) -> pfrep_left_trim_aligned_result_witness_output=pfrep_right_trim_aligned_result_witness_output)))))))))))))