FpPolynomialAlignedSubtract(p,ab,ac,L,bb,bc,M,rb,rc,N)

((forall fom_index_pfp_working_aligned_definition_left_bounded. (exists fom_gap_pfp_working_aligned_definition_left_bounded_index_bound. fom_gap_pfp_working_aligned_definition_left_bounded_index_bound + S (fom_index_pfp_working_aligned_definition_left_bounded) = (M)) -> exists fom_value_pfp_working_aligned_definition_left_bounded. ((((exists fom_beta_height_pfp_working_aligned_definition_left_bounded_entry. fom_beta_height_pfp_working_aligned_definition_left_bounded_entry + S (fom_value_pfp_working_aligned_definition_left_bounded) = S ((S (fom_index_pfp_working_aligned_definition_left_bounded)) * (bc))) /\ exists fom_beta_quotient_pfp_working_aligned_definition_left_bounded_entry. (bb) = fom_beta_quotient_pfp_working_aligned_definition_left_bounded_entry * S ((S (fom_index_pfp_working_aligned_definition_left_bounded)) * (bc)) + (fom_value_pfp_working_aligned_definition_left_bounded))) /\ (exists fom_gap_pfp_working_aligned_definition_left_bounded_value_bound. fom_gap_pfp_working_aligned_definition_left_bounded_value_bound + S (fom_value_pfp_working_aligned_definition_left_bounded) = (p)))) /\ (((forall fom_index_pfp_working_aligned_definition_right_bounded. (exists fom_gap_pfp_working_aligned_definition_right_bounded_index_bound. fom_gap_pfp_working_aligned_definition_right_bounded_index_bound + S (fom_index_pfp_working_aligned_definition_right_bounded) = (N)) -> exists fom_value_pfp_working_aligned_definition_right_bounded. ((((exists fom_beta_height_pfp_working_aligned_definition_right_bounded_entry. fom_beta_height_pfp_working_aligned_definition_right_bounded_entry + S (fom_value_pfp_working_aligned_definition_right_bounded) = S ((S (fom_index_pfp_working_aligned_definition_right_bounded)) * (rc))) /\ exists fom_beta_quotient_pfp_working_aligned_definition_right_bounded_entry. (rb) = fom_beta_quotient_pfp_working_aligned_definition_right_bounded_entry * S ((S (fom_index_pfp_working_aligned_definition_right_bounded)) * (rc)) + (fom_value_pfp_working_aligned_definition_right_bounded))) /\ (exists fom_gap_pfp_working_aligned_definition_right_bounded_value_bound. fom_gap_pfp_working_aligned_definition_right_bounded_value_bound + S (fom_value_pfp_working_aligned_definition_right_bounded) = (p)))) /\ (((forall fom_index_pfp_working_aligned_definition_result_bounded. (exists fom_gap_pfp_working_aligned_definition_result_bounded_index_bound. fom_gap_pfp_working_aligned_definition_result_bounded_index_bound + S (fom_index_pfp_working_aligned_definition_result_bounded) = (L)) -> exists fom_value_pfp_working_aligned_definition_result_bounded. ((((exists fom_beta_height_pfp_working_aligned_definition_result_bounded_entry. fom_beta_height_pfp_working_aligned_definition_result_bounded_entry + S (fom_value_pfp_working_aligned_definition_result_bounded) = S ((S (fom_index_pfp_working_aligned_definition_result_bounded)) * (ac))) /\ exists fom_beta_quotient_pfp_working_aligned_definition_result_bounded_entry. (ab) = fom_beta_quotient_pfp_working_aligned_definition_result_bounded_entry * S ((S (fom_index_pfp_working_aligned_definition_result_bounded)) * (ac)) + (fom_value_pfp_working_aligned_definition_result_bounded))) /\ (exists fom_gap_pfp_working_aligned_definition_result_bounded_value_bound. fom_gap_pfp_working_aligned_definition_result_bounded_value_bound + S (fom_value_pfp_working_aligned_definition_result_bounded) = (p)))) /\ ((exists pfaa_left_b_working_aligned_definition pfaa_left_c_working_aligned_definition pfaa_right_b_working_aligned_definition pfaa_right_c_working_aligned_definition pfaa_sum_b_working_aligned_definition pfaa_sum_c_working_aligned_definition pfaa_length_working_aligned_definition. ((((forall pfrep_power_working_aligned_definition_witness_common_left pfrep_left_working_aligned_definition_witness_common_left pfrep_right_working_aligned_definition_witness_common_left. ((exists pfrep_position_working_aligned_definition_witness_common_leftfirst. ((pfrep_position_working_aligned_definition_witness_common_leftfirst+S (pfrep_power_working_aligned_definition_witness_common_left)=((M))) /\ ((((exists ff_h_pfp_working_aligned_definition_witness_common_leftfirstentry. ff_h_pfp_working_aligned_definition_witness_common_leftfirstentry + S (pfrep_left_working_aligned_definition_witness_common_left) = S ((S (pfrep_position_working_aligned_definition_witness_common_leftfirst)) * (bc))) /\ exists ff_q_pfp_working_aligned_definition_witness_common_leftfirstentry. (bb) = ff_q_pfp_working_aligned_definition_witness_common_leftfirstentry * S ((S (pfrep_position_working_aligned_definition_witness_common_leftfirst)) * (bc)) + (pfrep_left_working_aligned_definition_witness_common_left)))))) \/ (((exists pfrep_gap_working_aligned_definition_witness_common_leftfirstoutside. pfrep_gap_working_aligned_definition_witness_common_leftfirstoutside+((M))=(pfrep_power_working_aligned_definition_witness_common_left)) /\ (((pfrep_left_working_aligned_definition_witness_common_left)=0))))) -> ((exists pfrep_position_working_aligned_definition_witness_common_leftsecond. ((pfrep_position_working_aligned_definition_witness_common_leftsecond+S (pfrep_power_working_aligned_definition_witness_common_left)=(pfaa_length_working_aligned_definition)) /\ ((((exists ff_h_pfp_working_aligned_definition_witness_common_leftsecondentry. ff_h_pfp_working_aligned_definition_witness_common_leftsecondentry + S (pfrep_right_working_aligned_definition_witness_common_left) = S ((S (pfrep_position_working_aligned_definition_witness_common_leftsecond)) * pfaa_left_c_working_aligned_definition)) /\ exists ff_q_pfp_working_aligned_definition_witness_common_leftsecondentry. pfaa_left_b_working_aligned_definition = ff_q_pfp_working_aligned_definition_witness_common_leftsecondentry * S ((S (pfrep_position_working_aligned_definition_witness_common_leftsecond)) * pfaa_left_c_working_aligned_definition) + (pfrep_right_working_aligned_definition_witness_common_left)))))) \/ (((exists pfrep_gap_working_aligned_definition_witness_common_leftsecondoutside. pfrep_gap_working_aligned_definition_witness_common_leftsecondoutside+(pfaa_length_working_aligned_definition)=(pfrep_power_working_aligned_definition_witness_common_left)) /\ (((pfrep_right_working_aligned_definition_witness_common_left)=0))))) -> pfrep_left_working_aligned_definition_witness_common_left=pfrep_right_working_aligned_definition_witness_common_left) /\ ((forall pfrep_power_working_aligned_definition_witness_common_right pfrep_left_working_aligned_definition_witness_common_right pfrep_right_working_aligned_definition_witness_common_right. ((exists pfrep_position_working_aligned_definition_witness_common_rightfirst. ((pfrep_position_working_aligned_definition_witness_common_rightfirst+S (pfrep_power_working_aligned_definition_witness_common_right)=((N))) /\ ((((exists ff_h_pfp_working_aligned_definition_witness_common_rightfirstentry. ff_h_pfp_working_aligned_definition_witness_common_rightfirstentry + S (pfrep_left_working_aligned_definition_witness_common_right) = S ((S (pfrep_position_working_aligned_definition_witness_common_rightfirst)) * (rc))) /\ exists ff_q_pfp_working_aligned_definition_witness_common_rightfirstentry. (rb) = ff_q_pfp_working_aligned_definition_witness_common_rightfirstentry * S ((S (pfrep_position_working_aligned_definition_witness_common_rightfirst)) * (rc)) + (pfrep_left_working_aligned_definition_witness_common_right)))))) \/ (((exists pfrep_gap_working_aligned_definition_witness_common_rightfirstoutside. pfrep_gap_working_aligned_definition_witness_common_rightfirstoutside+((N))=(pfrep_power_working_aligned_definition_witness_common_right)) /\ (((pfrep_left_working_aligned_definition_witness_common_right)=0))))) -> ((exists pfrep_position_working_aligned_definition_witness_common_rightsecond. ((pfrep_position_working_aligned_definition_witness_common_rightsecond+S (pfrep_power_working_aligned_definition_witness_common_right)=(pfaa_length_working_aligned_definition)) /\ ((((exists ff_h_pfp_working_aligned_definition_witness_common_rightsecondentry. ff_h_pfp_working_aligned_definition_witness_common_rightsecondentry + S (pfrep_right_working_aligned_definition_witness_common_right) = S ((S (pfrep_position_working_aligned_definition_witness_common_rightsecond)) * pfaa_right_c_working_aligned_definition)) /\ exists ff_q_pfp_working_aligned_definition_witness_common_rightsecondentry. pfaa_right_b_working_aligned_definition = ff_q_pfp_working_aligned_definition_witness_common_rightsecondentry * S ((S (pfrep_position_working_aligned_definition_witness_common_rightsecond)) * pfaa_right_c_working_aligned_definition) + (pfrep_right_working_aligned_definition_witness_common_right)))))) \/ (((exists pfrep_gap_working_aligned_definition_witness_common_rightsecondoutside. pfrep_gap_working_aligned_definition_witness_common_rightsecondoutside+(pfaa_length_working_aligned_definition)=(pfrep_power_working_aligned_definition_witness_common_right)) /\ (((pfrep_right_working_aligned_definition_witness_common_right)=0))))) -> pfrep_left_working_aligned_definition_witness_common_right=pfrep_right_working_aligned_definition_witness_common_right)))) /\ (((forall pfp_index_working_aligned_definition_witness_operation. (exists pfa_gap_working_aligned_definition_witness_operationindex. pfa_gap_working_aligned_definition_witness_operationindex + S (pfp_index_working_aligned_definition_witness_operation) = (pfaa_length_working_aligned_definition)) -> exists pfp_left_working_aligned_definition_witness_operation pfp_right_working_aligned_definition_witness_operation pfp_value_working_aligned_definition_witness_operation. ((((exists ff_h_pfp_working_aligned_definition_witness_operationleft. ff_h_pfp_working_aligned_definition_witness_operationleft + S (pfp_left_working_aligned_definition_witness_operation) = S ((S (pfp_index_working_aligned_definition_witness_operation)) * pfaa_left_c_working_aligned_definition)) /\ exists ff_q_pfp_working_aligned_definition_witness_operationleft. pfaa_left_b_working_aligned_definition = ff_q_pfp_working_aligned_definition_witness_operationleft * S ((S (pfp_index_working_aligned_definition_witness_operation)) * pfaa_left_c_working_aligned_definition) + (pfp_left_working_aligned_definition_witness_operation))) /\ (((((exists ff_h_pfp_working_aligned_definition_witness_operationright. ff_h_pfp_working_aligned_definition_witness_operationright + S (pfp_right_working_aligned_definition_witness_operation) = S ((S (pfp_index_working_aligned_definition_witness_operation)) * pfaa_right_c_working_aligned_definition)) /\ exists ff_q_pfp_working_aligned_definition_witness_operationright. pfaa_right_b_working_aligned_definition = ff_q_pfp_working_aligned_definition_witness_operationright * S ((S (pfp_index_working_aligned_definition_witness_operation)) * pfaa_right_c_working_aligned_definition) + (pfp_right_working_aligned_definition_witness_operation))) /\ (((((exists ff_h_pfp_working_aligned_definition_witness_operationtarget. ff_h_pfp_working_aligned_definition_witness_operationtarget + S (pfp_value_working_aligned_definition_witness_operation) = S ((S (pfp_index_working_aligned_definition_witness_operation)) * pfaa_sum_c_working_aligned_definition)) /\ exists ff_q_pfp_working_aligned_definition_witness_operationtarget. pfaa_sum_b_working_aligned_definition = ff_q_pfp_working_aligned_definition_witness_operationtarget * S ((S (pfp_index_working_aligned_definition_witness_operation)) * pfaa_sum_c_working_aligned_definition) + (pfp_value_working_aligned_definition_witness_operation))) /\ ((((exists pfa_gap_working_aligned_definition_witness_operationoperationleft. pfa_gap_working_aligned_definition_witness_operationoperationleft + S (pfp_left_working_aligned_definition_witness_operation) = ((p))) /\ (((exists pfa_gap_working_aligned_definition_witness_operationoperationright. pfa_gap_working_aligned_definition_witness_operationoperationright + S (pfp_right_working_aligned_definition_witness_operation) = ((p))) /\ ((((exists pfa_gap_working_aligned_definition_witness_operationoperationresultbound. pfa_gap_working_aligned_definition_witness_operationoperationresultbound + S (pfp_value_working_aligned_definition_witness_operation) = ((p))) /\ ((exists pfa_offset_left_working_aligned_definition_witness_operationoperationresultcongruence pfa_offset_right_working_aligned_definition_witness_operationoperationresultcongruence. ((pfp_left_working_aligned_definition_witness_operation) + (pfp_right_working_aligned_definition_witness_operation)) + ((p)) * pfa_offset_left_working_aligned_definition_witness_operationoperationresultcongruence = (pfp_value_working_aligned_definition_witness_operation) + ((p)) * pfa_offset_right_working_aligned_definition_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_working_aligned_definition_witness_output pfrep_left_working_aligned_definition_witness_output pfrep_right_working_aligned_definition_witness_output. ((exists pfrep_position_working_aligned_definition_witness_outputfirst. ((pfrep_position_working_aligned_definition_witness_outputfirst+S (pfrep_power_working_aligned_definition_witness_output)=(pfaa_length_working_aligned_definition)) /\ ((((exists ff_h_pfp_working_aligned_definition_witness_outputfirstentry. ff_h_pfp_working_aligned_definition_witness_outputfirstentry + S (pfrep_left_working_aligned_definition_witness_output) = S ((S (pfrep_position_working_aligned_definition_witness_outputfirst)) * pfaa_sum_c_working_aligned_definition)) /\ exists ff_q_pfp_working_aligned_definition_witness_outputfirstentry. pfaa_sum_b_working_aligned_definition = ff_q_pfp_working_aligned_definition_witness_outputfirstentry * S ((S (pfrep_position_working_aligned_definition_witness_outputfirst)) * pfaa_sum_c_working_aligned_definition) + (pfrep_left_working_aligned_definition_witness_output)))))) \/ (((exists pfrep_gap_working_aligned_definition_witness_outputfirstoutside. pfrep_gap_working_aligned_definition_witness_outputfirstoutside+(pfaa_length_working_aligned_definition)=(pfrep_power_working_aligned_definition_witness_output)) /\ (((pfrep_left_working_aligned_definition_witness_output)=0))))) -> ((exists pfrep_position_working_aligned_definition_witness_outputsecond. ((pfrep_position_working_aligned_definition_witness_outputsecond+S (pfrep_power_working_aligned_definition_witness_output)=((L))) /\ ((((exists ff_h_pfp_working_aligned_definition_witness_outputsecondentry. ff_h_pfp_working_aligned_definition_witness_outputsecondentry + S (pfrep_right_working_aligned_definition_witness_output) = S ((S (pfrep_position_working_aligned_definition_witness_outputsecond)) * (ac))) /\ exists ff_q_pfp_working_aligned_definition_witness_outputsecondentry. (ab) = ff_q_pfp_working_aligned_definition_witness_outputsecondentry * S ((S (pfrep_position_working_aligned_definition_witness_outputsecond)) * (ac)) + (pfrep_right_working_aligned_definition_witness_output)))))) \/ (((exists pfrep_gap_working_aligned_definition_witness_outputsecondoutside. pfrep_gap_working_aligned_definition_witness_outputsecondoutside+((L))=(pfrep_power_working_aligned_definition_witness_output)) /\ (((pfrep_right_working_aligned_definition_witness_output)=0))))) -> pfrep_left_working_aligned_definition_witness_output=pfrep_right_working_aligned_definition_witness_output))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.