FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,q)

exists pfd_input_working_euclidean_definition pfd_previous_working_euclidean_definition pfd_difference_working_euclidean_definition. ((((exists ff_h_pfp_working_euclidean_definitioninput. ff_h_pfp_working_euclidean_definitioninput + S (pfd_input_working_euclidean_definition) = S ((S ((i))) * (ac))) /\ exists ff_q_pfp_working_euclidean_definitioninput. (ab) = ff_q_pfp_working_euclidean_definitioninput * S ((S ((i))) * (ac)) + (pfd_input_working_euclidean_definition))) /\ (((exists pfc_terms_code_working_euclidean_definitionprevious pfc_terms_scale_working_euclidean_definitionprevious pfc_natural_sum_working_euclidean_definitionprevious. ((forall pfc_index_working_euclidean_definitionpreviousdiagonal. (exists pfa_gap_working_euclidean_definitionpreviousdiagonalbound. pfa_gap_working_euclidean_definitionpreviousdiagonalbound + S (pfc_index_working_euclidean_definitionpreviousdiagonal) = (S ((i)))) -> exists pfc_value_working_euclidean_definitionpreviousdiagonal. ((((exists ff_h_pfp_working_euclidean_definitionpreviousdiagonalentry. ff_h_pfp_working_euclidean_definitionpreviousdiagonalentry + S (pfc_value_working_euclidean_definitionpreviousdiagonal) = S ((S (pfc_index_working_euclidean_definitionpreviousdiagonal)) * pfc_terms_scale_working_euclidean_definitionprevious)) /\ exists ff_q_pfp_working_euclidean_definitionpreviousdiagonalentry. pfc_terms_code_working_euclidean_definitionprevious = ff_q_pfp_working_euclidean_definitionpreviousdiagonalentry * S ((S (pfc_index_working_euclidean_definitionpreviousdiagonal)) * pfc_terms_scale_working_euclidean_definitionprevious) + (pfc_value_working_euclidean_definitionpreviousdiagonal))) /\ ((exists pfc_complement_working_euclidean_definitionpreviousdiagonalterm pfc_left_working_euclidean_definitionpreviousdiagonalterm pfc_right_working_euclidean_definitionpreviousdiagonalterm. (((pfc_index_working_euclidean_definitionpreviousdiagonal)+pfc_complement_working_euclidean_definitionpreviousdiagonalterm=((i))) /\ ((((((exists pfa_gap_working_euclidean_definitionpreviousdiagonaltermleftinside. pfa_gap_working_euclidean_definitionpreviousdiagonaltermleftinside + S (pfc_index_working_euclidean_definitionpreviousdiagonal) = ((i))) /\ ((((exists ff_h_pfp_working_euclidean_definitionpreviousdiagonaltermleftentry. ff_h_pfp_working_euclidean_definitionpreviousdiagonaltermleftentry + S (pfc_left_working_euclidean_definitionpreviousdiagonalterm) = S ((S (pfc_index_working_euclidean_definitionpreviousdiagonal)) * (qc))) /\ exists ff_q_pfp_working_euclidean_definitionpreviousdiagonaltermleftentry. (qb) = ff_q_pfp_working_euclidean_definitionpreviousdiagonaltermleftentry * S ((S (pfc_index_working_euclidean_definitionpreviousdiagonal)) * (qc)) + (pfc_left_working_euclidean_definitionpreviousdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definitionpreviousdiagonaltermleftoutside. pfc_gap_working_euclidean_definitionpreviousdiagonaltermleftoutside+((i))=(pfc_index_working_euclidean_definitionpreviousdiagonal)) /\ (((pfc_left_working_euclidean_definitionpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_working_euclidean_definitionpreviousdiagonaltermrightinside. pfa_gap_working_euclidean_definitionpreviousdiagonaltermrightinside + S (pfc_complement_working_euclidean_definitionpreviousdiagonalterm) = ((M))) /\ ((((exists ff_h_pfp_working_euclidean_definitionpreviousdiagonaltermrightentry. ff_h_pfp_working_euclidean_definitionpreviousdiagonaltermrightentry + S (pfc_right_working_euclidean_definitionpreviousdiagonalterm) = S ((S (pfc_complement_working_euclidean_definitionpreviousdiagonalterm)) * (bc))) /\ exists ff_q_pfp_working_euclidean_definitionpreviousdiagonaltermrightentry. (bb) = ff_q_pfp_working_euclidean_definitionpreviousdiagonaltermrightentry * S ((S (pfc_complement_working_euclidean_definitionpreviousdiagonalterm)) * (bc)) + (pfc_right_working_euclidean_definitionpreviousdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definitionpreviousdiagonaltermrightoutside. pfc_gap_working_euclidean_definitionpreviousdiagonaltermrightoutside+((M))=(pfc_complement_working_euclidean_definitionpreviousdiagonalterm)) /\ (((pfc_right_working_euclidean_definitionpreviousdiagonalterm)=0))))) /\ (((pfc_value_working_euclidean_definitionpreviousdiagonal)=pfc_left_working_euclidean_definitionpreviousdiagonalterm*pfc_right_working_euclidean_definitionpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_working_euclidean_definitionprevioussum fs_v_pfc_working_euclidean_definitionprevioussum. ((((exists fs_h_pfc_working_euclidean_definitionprevioussum_body_start. fs_h_pfc_working_euclidean_definitionprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_working_euclidean_definitionprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionprevioussum_body_start. fs_u_pfc_working_euclidean_definitionprevioussum = fs_q_pfc_working_euclidean_definitionprevioussum_body_start * S ((S (0)) * fs_v_pfc_working_euclidean_definitionprevioussum) + (0))) /\ ((((exists fs_h_pfc_working_euclidean_definitionprevioussum_body_terminal. fs_h_pfc_working_euclidean_definitionprevioussum_body_terminal + S (pfc_natural_sum_working_euclidean_definitionprevious) = S ((S (S ((i)))) * fs_v_pfc_working_euclidean_definitionprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionprevioussum_body_terminal. fs_u_pfc_working_euclidean_definitionprevioussum = fs_q_pfc_working_euclidean_definitionprevioussum_body_terminal * S ((S (S ((i)))) * fs_v_pfc_working_euclidean_definitionprevioussum) + (pfc_natural_sum_working_euclidean_definitionprevious))) /\ forall fs_i_pfc_working_euclidean_definitionprevioussum_body_steps. (exists fs_lt_pfc_working_euclidean_definitionprevioussum_body_steps_bound. fs_lt_pfc_working_euclidean_definitionprevioussum_body_steps_bound + S fs_i_pfc_working_euclidean_definitionprevioussum_body_steps = S ((i))) -> exists fs_a_pfc_working_euclidean_definitionprevioussum_body_steps fs_r_pfc_working_euclidean_definitionprevioussum_body_steps fs_s_pfc_working_euclidean_definitionprevioussum_body_steps. ((((exists fs_h_pfc_working_euclidean_definitionprevioussum_body_steps_summand. fs_h_pfc_working_euclidean_definitionprevioussum_body_steps_summand + S (fs_a_pfc_working_euclidean_definitionprevioussum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definitionprevioussum_body_steps)) * pfc_terms_scale_working_euclidean_definitionprevious)) /\ exists fs_q_pfc_working_euclidean_definitionprevioussum_body_steps_summand. pfc_terms_code_working_euclidean_definitionprevious = fs_q_pfc_working_euclidean_definitionprevioussum_body_steps_summand * S ((S (fs_i_pfc_working_euclidean_definitionprevioussum_body_steps)) * pfc_terms_scale_working_euclidean_definitionprevious) + (fs_a_pfc_working_euclidean_definitionprevioussum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definitionprevioussum_body_steps_partial. fs_h_pfc_working_euclidean_definitionprevioussum_body_steps_partial + S (fs_r_pfc_working_euclidean_definitionprevioussum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definitionprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionprevioussum_body_steps_partial. fs_u_pfc_working_euclidean_definitionprevioussum = fs_q_pfc_working_euclidean_definitionprevioussum_body_steps_partial * S ((S (fs_i_pfc_working_euclidean_definitionprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionprevioussum) + (fs_r_pfc_working_euclidean_definitionprevioussum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definitionprevioussum_body_steps_successor. fs_h_pfc_working_euclidean_definitionprevioussum_body_steps_successor + S (fs_s_pfc_working_euclidean_definitionprevioussum_body_steps) = S ((S (S fs_i_pfc_working_euclidean_definitionprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionprevioussum_body_steps_successor. fs_u_pfc_working_euclidean_definitionprevioussum = fs_q_pfc_working_euclidean_definitionprevioussum_body_steps_successor * S ((S (S fs_i_pfc_working_euclidean_definitionprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionprevioussum) + (fs_s_pfc_working_euclidean_definitionprevioussum_body_steps))) /\ fs_s_pfc_working_euclidean_definitionprevioussum_body_steps = fs_r_pfc_working_euclidean_definitionprevioussum_body_steps + fs_a_pfc_working_euclidean_definitionprevioussum_body_steps)))))) /\ ((((exists pfa_gap_working_euclidean_definitionpreviousresiduebound. pfa_gap_working_euclidean_definitionpreviousresiduebound + S (pfd_previous_working_euclidean_definition) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionpreviousresiduecongruence pfa_offset_right_working_euclidean_definitionpreviousresiduecongruence. (pfc_natural_sum_working_euclidean_definitionprevious) + ((p)) * pfa_offset_left_working_euclidean_definitionpreviousresiduecongruence = (pfd_previous_working_euclidean_definition) + ((p)) * pfa_offset_right_working_euclidean_definitionpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_working_euclidean_definitionsubtractleft. pfa_gap_working_euclidean_definitionsubtractleft + S (pfd_previous_working_euclidean_definition) = ((p))) /\ (((exists pfa_gap_working_euclidean_definitionsubtractright. pfa_gap_working_euclidean_definitionsubtractright + S (pfd_difference_working_euclidean_definition) = ((p))) /\ ((((exists pfa_gap_working_euclidean_definitionsubtractresultbound. pfa_gap_working_euclidean_definitionsubtractresultbound + S (pfd_input_working_euclidean_definition) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionsubtractresultcongruence pfa_offset_right_working_euclidean_definitionsubtractresultcongruence. ((pfd_previous_working_euclidean_definition) + (pfd_difference_working_euclidean_definition)) + ((p)) * pfa_offset_left_working_euclidean_definitionsubtractresultcongruence = (pfd_input_working_euclidean_definition) + ((p)) * pfa_offset_right_working_euclidean_definitionsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_working_euclidean_definitionmultiplyleft. pfa_gap_working_euclidean_definitionmultiplyleft + S ((k)) = ((p))) /\ (((exists pfa_gap_working_euclidean_definitionmultiplyright. pfa_gap_working_euclidean_definitionmultiplyright + S (pfd_difference_working_euclidean_definition) = ((p))) /\ ((((exists pfa_gap_working_euclidean_definitionmultiplyresultbound. pfa_gap_working_euclidean_definitionmultiplyresultbound + S ((q)) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionmultiplyresultcongruence pfa_offset_right_working_euclidean_definitionmultiplyresultcongruence. (((k)) * (pfd_difference_working_euclidean_definition)) + ((p)) * pfa_offset_left_working_euclidean_definitionmultiplyresultcongruence = ((q)) + ((p)) * pfa_offset_right_working_euclidean_definitionmultiplyresultcongruence)))))))))))))))

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