FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N)

forall pfd_index_working_euclidean_definition. (exists pfa_gap_working_euclidean_definitionbound. pfa_gap_working_euclidean_definitionbound + S (pfd_index_working_euclidean_definition) = ((N))) -> exists pfd_value_working_euclidean_definition. ((((exists ff_h_pfp_working_euclidean_definitionentry. ff_h_pfp_working_euclidean_definitionentry + S (pfd_value_working_euclidean_definition) = S ((S (pfd_index_working_euclidean_definition)) * (qc))) /\ exists ff_q_pfp_working_euclidean_definitionentry. (qb) = ff_q_pfp_working_euclidean_definitionentry * S ((S (pfd_index_working_euclidean_definition)) * (qc)) + (pfd_value_working_euclidean_definition))) /\ ((exists pfd_input_working_euclidean_definitionstep pfd_previous_working_euclidean_definitionstep pfd_difference_working_euclidean_definitionstep. ((((exists ff_h_pfp_working_euclidean_definitionstepinput. ff_h_pfp_working_euclidean_definitionstepinput + S (pfd_input_working_euclidean_definitionstep) = S ((S (pfd_index_working_euclidean_definition)) * (ac))) /\ exists ff_q_pfp_working_euclidean_definitionstepinput. (ab) = ff_q_pfp_working_euclidean_definitionstepinput * S ((S (pfd_index_working_euclidean_definition)) * (ac)) + (pfd_input_working_euclidean_definitionstep))) /\ (((exists pfc_terms_code_working_euclidean_definitionstepprevious pfc_terms_scale_working_euclidean_definitionstepprevious pfc_natural_sum_working_euclidean_definitionstepprevious. ((forall pfc_index_working_euclidean_definitionsteppreviousdiagonal. (exists pfa_gap_working_euclidean_definitionsteppreviousdiagonalbound. pfa_gap_working_euclidean_definitionsteppreviousdiagonalbound + S (pfc_index_working_euclidean_definitionsteppreviousdiagonal) = (S (pfd_index_working_euclidean_definition))) -> exists pfc_value_working_euclidean_definitionsteppreviousdiagonal. ((((exists ff_h_pfp_working_euclidean_definitionsteppreviousdiagonalentry. ff_h_pfp_working_euclidean_definitionsteppreviousdiagonalentry + S (pfc_value_working_euclidean_definitionsteppreviousdiagonal) = S ((S (pfc_index_working_euclidean_definitionsteppreviousdiagonal)) * pfc_terms_scale_working_euclidean_definitionstepprevious)) /\ exists ff_q_pfp_working_euclidean_definitionsteppreviousdiagonalentry. pfc_terms_code_working_euclidean_definitionstepprevious = ff_q_pfp_working_euclidean_definitionsteppreviousdiagonalentry * S ((S (pfc_index_working_euclidean_definitionsteppreviousdiagonal)) * pfc_terms_scale_working_euclidean_definitionstepprevious) + (pfc_value_working_euclidean_definitionsteppreviousdiagonal))) /\ ((exists pfc_complement_working_euclidean_definitionsteppreviousdiagonalterm pfc_left_working_euclidean_definitionsteppreviousdiagonalterm pfc_right_working_euclidean_definitionsteppreviousdiagonalterm. (((pfc_index_working_euclidean_definitionsteppreviousdiagonal)+pfc_complement_working_euclidean_definitionsteppreviousdiagonalterm=(pfd_index_working_euclidean_definition)) /\ ((((((exists pfa_gap_working_euclidean_definitionsteppreviousdiagonaltermleftinside. pfa_gap_working_euclidean_definitionsteppreviousdiagonaltermleftinside + S (pfc_index_working_euclidean_definitionsteppreviousdiagonal) = (pfd_index_working_euclidean_definition)) /\ ((((exists ff_h_pfp_working_euclidean_definitionsteppreviousdiagonaltermleftentry. ff_h_pfp_working_euclidean_definitionsteppreviousdiagonaltermleftentry + S (pfc_left_working_euclidean_definitionsteppreviousdiagonalterm) = S ((S (pfc_index_working_euclidean_definitionsteppreviousdiagonal)) * (qc))) /\ exists ff_q_pfp_working_euclidean_definitionsteppreviousdiagonaltermleftentry. (qb) = ff_q_pfp_working_euclidean_definitionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_working_euclidean_definitionsteppreviousdiagonal)) * (qc)) + (pfc_left_working_euclidean_definitionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definitionsteppreviousdiagonaltermleftoutside. pfc_gap_working_euclidean_definitionsteppreviousdiagonaltermleftoutside+(pfd_index_working_euclidean_definition)=(pfc_index_working_euclidean_definitionsteppreviousdiagonal)) /\ (((pfc_left_working_euclidean_definitionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_working_euclidean_definitionsteppreviousdiagonaltermrightinside. pfa_gap_working_euclidean_definitionsteppreviousdiagonaltermrightinside + S (pfc_complement_working_euclidean_definitionsteppreviousdiagonalterm) = ((M))) /\ ((((exists ff_h_pfp_working_euclidean_definitionsteppreviousdiagonaltermrightentry. ff_h_pfp_working_euclidean_definitionsteppreviousdiagonaltermrightentry + S (pfc_right_working_euclidean_definitionsteppreviousdiagonalterm) = S ((S (pfc_complement_working_euclidean_definitionsteppreviousdiagonalterm)) * (bc))) /\ exists ff_q_pfp_working_euclidean_definitionsteppreviousdiagonaltermrightentry. (bb) = ff_q_pfp_working_euclidean_definitionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_working_euclidean_definitionsteppreviousdiagonalterm)) * (bc)) + (pfc_right_working_euclidean_definitionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definitionsteppreviousdiagonaltermrightoutside. pfc_gap_working_euclidean_definitionsteppreviousdiagonaltermrightoutside+((M))=(pfc_complement_working_euclidean_definitionsteppreviousdiagonalterm)) /\ (((pfc_right_working_euclidean_definitionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_working_euclidean_definitionsteppreviousdiagonal)=pfc_left_working_euclidean_definitionsteppreviousdiagonalterm*pfc_right_working_euclidean_definitionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_working_euclidean_definitionstepprevioussum fs_v_pfc_working_euclidean_definitionstepprevioussum. ((((exists fs_h_pfc_working_euclidean_definitionstepprevioussum_body_start. fs_h_pfc_working_euclidean_definitionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_working_euclidean_definitionstepprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionstepprevioussum_body_start. fs_u_pfc_working_euclidean_definitionstepprevioussum = fs_q_pfc_working_euclidean_definitionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_working_euclidean_definitionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_working_euclidean_definitionstepprevioussum_body_terminal. fs_h_pfc_working_euclidean_definitionstepprevioussum_body_terminal + S (pfc_natural_sum_working_euclidean_definitionstepprevious) = S ((S (S (pfd_index_working_euclidean_definition))) * fs_v_pfc_working_euclidean_definitionstepprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionstepprevioussum_body_terminal. fs_u_pfc_working_euclidean_definitionstepprevioussum = fs_q_pfc_working_euclidean_definitionstepprevioussum_body_terminal * S ((S (S (pfd_index_working_euclidean_definition))) * fs_v_pfc_working_euclidean_definitionstepprevioussum) + (pfc_natural_sum_working_euclidean_definitionstepprevious))) /\ forall fs_i_pfc_working_euclidean_definitionstepprevioussum_body_steps. (exists fs_lt_pfc_working_euclidean_definitionstepprevioussum_body_steps_bound. fs_lt_pfc_working_euclidean_definitionstepprevioussum_body_steps_bound + S fs_i_pfc_working_euclidean_definitionstepprevioussum_body_steps = S (pfd_index_working_euclidean_definition)) -> exists fs_a_pfc_working_euclidean_definitionstepprevioussum_body_steps fs_r_pfc_working_euclidean_definitionstepprevioussum_body_steps fs_s_pfc_working_euclidean_definitionstepprevioussum_body_steps. ((((exists fs_h_pfc_working_euclidean_definitionstepprevioussum_body_steps_summand. fs_h_pfc_working_euclidean_definitionstepprevioussum_body_steps_summand + S (fs_a_pfc_working_euclidean_definitionstepprevioussum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definitionstepprevioussum_body_steps)) * pfc_terms_scale_working_euclidean_definitionstepprevious)) /\ exists fs_q_pfc_working_euclidean_definitionstepprevioussum_body_steps_summand. pfc_terms_code_working_euclidean_definitionstepprevious = fs_q_pfc_working_euclidean_definitionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_working_euclidean_definitionstepprevioussum_body_steps)) * pfc_terms_scale_working_euclidean_definitionstepprevious) + (fs_a_pfc_working_euclidean_definitionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definitionstepprevioussum_body_steps_partial. fs_h_pfc_working_euclidean_definitionstepprevioussum_body_steps_partial + S (fs_r_pfc_working_euclidean_definitionstepprevioussum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definitionstepprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionstepprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionstepprevioussum_body_steps_partial. fs_u_pfc_working_euclidean_definitionstepprevioussum = fs_q_pfc_working_euclidean_definitionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_working_euclidean_definitionstepprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionstepprevioussum) + (fs_r_pfc_working_euclidean_definitionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definitionstepprevioussum_body_steps_successor. fs_h_pfc_working_euclidean_definitionstepprevioussum_body_steps_successor + S (fs_s_pfc_working_euclidean_definitionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_working_euclidean_definitionstepprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionstepprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionstepprevioussum_body_steps_successor. fs_u_pfc_working_euclidean_definitionstepprevioussum = fs_q_pfc_working_euclidean_definitionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_working_euclidean_definitionstepprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionstepprevioussum) + (fs_s_pfc_working_euclidean_definitionstepprevioussum_body_steps))) /\ fs_s_pfc_working_euclidean_definitionstepprevioussum_body_steps = fs_r_pfc_working_euclidean_definitionstepprevioussum_body_steps + fs_a_pfc_working_euclidean_definitionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_working_euclidean_definitionsteppreviousresiduebound. pfa_gap_working_euclidean_definitionsteppreviousresiduebound + S (pfd_previous_working_euclidean_definitionstep) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionsteppreviousresiduecongruence pfa_offset_right_working_euclidean_definitionsteppreviousresiduecongruence. (pfc_natural_sum_working_euclidean_definitionstepprevious) + ((p)) * pfa_offset_left_working_euclidean_definitionsteppreviousresiduecongruence = (pfd_previous_working_euclidean_definitionstep) + ((p)) * pfa_offset_right_working_euclidean_definitionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_working_euclidean_definitionstepsubtractleft. pfa_gap_working_euclidean_definitionstepsubtractleft + S (pfd_previous_working_euclidean_definitionstep) = ((p))) /\ (((exists pfa_gap_working_euclidean_definitionstepsubtractright. pfa_gap_working_euclidean_definitionstepsubtractright + S (pfd_difference_working_euclidean_definitionstep) = ((p))) /\ ((((exists pfa_gap_working_euclidean_definitionstepsubtractresultbound. pfa_gap_working_euclidean_definitionstepsubtractresultbound + S (pfd_input_working_euclidean_definitionstep) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionstepsubtractresultcongruence pfa_offset_right_working_euclidean_definitionstepsubtractresultcongruence. ((pfd_previous_working_euclidean_definitionstep) + (pfd_difference_working_euclidean_definitionstep)) + ((p)) * pfa_offset_left_working_euclidean_definitionstepsubtractresultcongruence = (pfd_input_working_euclidean_definitionstep) + ((p)) * pfa_offset_right_working_euclidean_definitionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_working_euclidean_definitionstepmultiplyleft. pfa_gap_working_euclidean_definitionstepmultiplyleft + S ((k)) = ((p))) /\ (((exists pfa_gap_working_euclidean_definitionstepmultiplyright. pfa_gap_working_euclidean_definitionstepmultiplyright + S (pfd_difference_working_euclidean_definitionstep) = ((p))) /\ ((((exists pfa_gap_working_euclidean_definitionstepmultiplyresultbound. pfa_gap_working_euclidean_definitionstepmultiplyresultbound + S (pfd_value_working_euclidean_definition) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionstepmultiplyresultcongruence pfa_offset_right_working_euclidean_definitionstepmultiplyresultcongruence. (((k)) * (pfd_difference_working_euclidean_definitionstep)) + ((p)) * pfa_offset_left_working_euclidean_definitionstepmultiplyresultcongruence = (pfd_value_working_euclidean_definition) + ((p)) * pfa_offset_right_working_euclidean_definitionstepmultiplyresultcongruence))))))))))))))))))

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