FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R)

((forall fom_index_pfp_working_euclidean_definitioninput. (exists fom_gap_pfp_working_euclidean_definitioninput_index_bound. fom_gap_pfp_working_euclidean_definitioninput_index_bound + S (fom_index_pfp_working_euclidean_definitioninput) = (L)) -> exists fom_value_pfp_working_euclidean_definitioninput. ((((exists fom_beta_height_pfp_working_euclidean_definitioninput_entry. fom_beta_height_pfp_working_euclidean_definitioninput_entry + S (fom_value_pfp_working_euclidean_definitioninput) = S ((S (fom_index_pfp_working_euclidean_definitioninput)) * (ac))) /\ exists fom_beta_quotient_pfp_working_euclidean_definitioninput_entry. (ab) = fom_beta_quotient_pfp_working_euclidean_definitioninput_entry * S ((S (fom_index_pfp_working_euclidean_definitioninput)) * (ac)) + (fom_value_pfp_working_euclidean_definitioninput))) /\ (exists fom_gap_pfp_working_euclidean_definitioninput_value_bound. fom_gap_pfp_working_euclidean_definitioninput_value_bound + S (fom_value_pfp_working_euclidean_definitioninput) = (p)))) /\ (((forall fom_index_pfp_working_euclidean_definitiondivisor. (exists fom_gap_pfp_working_euclidean_definitiondivisor_index_bound. fom_gap_pfp_working_euclidean_definitiondivisor_index_bound + S (fom_index_pfp_working_euclidean_definitiondivisor) = S ((d))) -> exists fom_value_pfp_working_euclidean_definitiondivisor. ((((exists fom_beta_height_pfp_working_euclidean_definitiondivisor_entry. fom_beta_height_pfp_working_euclidean_definitiondivisor_entry + S (fom_value_pfp_working_euclidean_definitiondivisor) = S ((S (fom_index_pfp_working_euclidean_definitiondivisor)) * (bc))) /\ exists fom_beta_quotient_pfp_working_euclidean_definitiondivisor_entry. (bb) = fom_beta_quotient_pfp_working_euclidean_definitiondivisor_entry * S ((S (fom_index_pfp_working_euclidean_definitiondivisor)) * (bc)) + (fom_value_pfp_working_euclidean_definitiondivisor))) /\ (exists fom_gap_pfp_working_euclidean_definitiondivisor_value_bound. fom_gap_pfp_working_euclidean_definitiondivisor_value_bound + S (fom_value_pfp_working_euclidean_definitiondivisor) = (p)))) /\ ((((((((q))=0) /\ ((exists pfc_gap_working_euclidean_definitionlengthshort. pfc_gap_working_euclidean_definitionlengthshort+((L))=((d)))))) \/ (((~(((q))=0)) /\ ((((q))+((d))=((L))))))) /\ ((exists pfd_head_working_euclidean_definition pfd_inverse_working_euclidean_definition pfd_product_code_working_euclidean_definition pfd_product_scale_working_euclidean_definition pfd_residual_code_working_euclidean_definition pfd_residual_scale_working_euclidean_definition pfd_cut_working_euclidean_definition. ((((exists ff_h_pfp_working_euclidean_definitionhead. ff_h_pfp_working_euclidean_definitionhead + S (pfd_head_working_euclidean_definition) = S ((S (0)) * (bc))) /\ exists ff_q_pfp_working_euclidean_definitionhead. (bb) = ff_q_pfp_working_euclidean_definitionhead * S ((S (0)) * (bc)) + (pfd_head_working_euclidean_definition))) /\ (((((~((pfd_head_working_euclidean_definition) = 0)) /\ ((((exists pfa_gap_working_euclidean_definitioninversemultiplicationleft. pfa_gap_working_euclidean_definitioninversemultiplicationleft + S (pfd_head_working_euclidean_definition) = ((p))) /\ (((exists pfa_gap_working_euclidean_definitioninversemultiplicationright. pfa_gap_working_euclidean_definitioninversemultiplicationright + S (pfd_inverse_working_euclidean_definition) = ((p))) /\ ((((exists pfa_gap_working_euclidean_definitioninversemultiplicationresultbound. pfa_gap_working_euclidean_definitioninversemultiplicationresultbound + S (1) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitioninversemultiplicationresultcongruence pfa_offset_right_working_euclidean_definitioninversemultiplicationresultcongruence. ((pfd_head_working_euclidean_definition) * (pfd_inverse_working_euclidean_definition)) + ((p)) * pfa_offset_left_working_euclidean_definitioninversemultiplicationresultcongruence = (1) + ((p)) * pfa_offset_right_working_euclidean_definitioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_working_euclidean_definitionquotient. (exists pfa_gap_working_euclidean_definitionquotientbound. pfa_gap_working_euclidean_definitionquotientbound + S (pfd_index_working_euclidean_definitionquotient) = ((q))) -> exists pfd_value_working_euclidean_definitionquotient. ((((exists ff_h_pfp_working_euclidean_definitionquotiententry. ff_h_pfp_working_euclidean_definitionquotiententry + S (pfd_value_working_euclidean_definitionquotient) = S ((S (pfd_index_working_euclidean_definitionquotient)) * (qc))) /\ exists ff_q_pfp_working_euclidean_definitionquotiententry. (qb) = ff_q_pfp_working_euclidean_definitionquotiententry * S ((S (pfd_index_working_euclidean_definitionquotient)) * (qc)) + (pfd_value_working_euclidean_definitionquotient))) /\ ((exists pfd_input_working_euclidean_definitionquotientstep pfd_previous_working_euclidean_definitionquotientstep pfd_difference_working_euclidean_definitionquotientstep. ((((exists ff_h_pfp_working_euclidean_definitionquotientstepinput. ff_h_pfp_working_euclidean_definitionquotientstepinput + S (pfd_input_working_euclidean_definitionquotientstep) = S ((S (pfd_index_working_euclidean_definitionquotient)) * (ac))) /\ exists ff_q_pfp_working_euclidean_definitionquotientstepinput. (ab) = ff_q_pfp_working_euclidean_definitionquotientstepinput * S ((S (pfd_index_working_euclidean_definitionquotient)) * (ac)) + (pfd_input_working_euclidean_definitionquotientstep))) /\ (((exists pfc_terms_code_working_euclidean_definitionquotientstepprevious pfc_terms_scale_working_euclidean_definitionquotientstepprevious pfc_natural_sum_working_euclidean_definitionquotientstepprevious. ((forall pfc_index_working_euclidean_definitionquotientsteppreviousdiagonal. (exists pfa_gap_working_euclidean_definitionquotientsteppreviousdiagonalbound. pfa_gap_working_euclidean_definitionquotientsteppreviousdiagonalbound + S (pfc_index_working_euclidean_definitionquotientsteppreviousdiagonal) = (S (pfd_index_working_euclidean_definitionquotient))) -> exists pfc_value_working_euclidean_definitionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_working_euclidean_definitionquotientsteppreviousdiagonalentry. ff_h_pfp_working_euclidean_definitionquotientsteppreviousdiagonalentry + S (pfc_value_working_euclidean_definitionquotientsteppreviousdiagonal) = S ((S (pfc_index_working_euclidean_definitionquotientsteppreviousdiagonal)) * pfc_terms_scale_working_euclidean_definitionquotientstepprevious)) /\ exists ff_q_pfp_working_euclidean_definitionquotientsteppreviousdiagonalentry. pfc_terms_code_working_euclidean_definitionquotientstepprevious = ff_q_pfp_working_euclidean_definitionquotientsteppreviousdiagonalentry * S ((S (pfc_index_working_euclidean_definitionquotientsteppreviousdiagonal)) * pfc_terms_scale_working_euclidean_definitionquotientstepprevious) + (pfc_value_working_euclidean_definitionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_working_euclidean_definitionquotientsteppreviousdiagonalterm pfc_left_working_euclidean_definitionquotientsteppreviousdiagonalterm pfc_right_working_euclidean_definitionquotientsteppreviousdiagonalterm. (((pfc_index_working_euclidean_definitionquotientsteppreviousdiagonal)+pfc_complement_working_euclidean_definitionquotientsteppreviousdiagonalterm=(pfd_index_working_euclidean_definitionquotient)) /\ ((((((exists pfa_gap_working_euclidean_definitionquotientsteppreviousdiagonaltermleftinside. pfa_gap_working_euclidean_definitionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_working_euclidean_definitionquotientsteppreviousdiagonal) = (pfd_index_working_euclidean_definitionquotient)) /\ ((((exists ff_h_pfp_working_euclidean_definitionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_working_euclidean_definitionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_working_euclidean_definitionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_working_euclidean_definitionquotientsteppreviousdiagonal)) * (qc))) /\ exists ff_q_pfp_working_euclidean_definitionquotientsteppreviousdiagonaltermleftentry. (qb) = ff_q_pfp_working_euclidean_definitionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_working_euclidean_definitionquotientsteppreviousdiagonal)) * (qc)) + (pfc_left_working_euclidean_definitionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definitionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_working_euclidean_definitionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_working_euclidean_definitionquotient)=(pfc_index_working_euclidean_definitionquotientsteppreviousdiagonal)) /\ (((pfc_left_working_euclidean_definitionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_working_euclidean_definitionquotientsteppreviousdiagonaltermrightinside. pfa_gap_working_euclidean_definitionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_working_euclidean_definitionquotientsteppreviousdiagonalterm) = (S ((d)))) /\ ((((exists ff_h_pfp_working_euclidean_definitionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_working_euclidean_definitionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_working_euclidean_definitionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_working_euclidean_definitionquotientsteppreviousdiagonalterm)) * (bc))) /\ exists ff_q_pfp_working_euclidean_definitionquotientsteppreviousdiagonaltermrightentry. (bb) = ff_q_pfp_working_euclidean_definitionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_working_euclidean_definitionquotientsteppreviousdiagonalterm)) * (bc)) + (pfc_right_working_euclidean_definitionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definitionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_working_euclidean_definitionquotientsteppreviousdiagonaltermrightoutside+(S ((d)))=(pfc_complement_working_euclidean_definitionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_working_euclidean_definitionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_working_euclidean_definitionquotientsteppreviousdiagonal)=pfc_left_working_euclidean_definitionquotientsteppreviousdiagonalterm*pfc_right_working_euclidean_definitionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_working_euclidean_definitionquotientstepprevioussum fs_v_pfc_working_euclidean_definitionquotientstepprevioussum. ((((exists fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_start. fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_working_euclidean_definitionquotientstepprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_start. fs_u_pfc_working_euclidean_definitionquotientstepprevioussum = fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_working_euclidean_definitionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_terminal. fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_working_euclidean_definitionquotientstepprevious) = S ((S (S (pfd_index_working_euclidean_definitionquotient))) * fs_v_pfc_working_euclidean_definitionquotientstepprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_terminal. fs_u_pfc_working_euclidean_definitionquotientstepprevioussum = fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_working_euclidean_definitionquotient))) * fs_v_pfc_working_euclidean_definitionquotientstepprevioussum) + (pfc_natural_sum_working_euclidean_definitionquotientstepprevious))) /\ forall fs_i_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps = S (pfd_index_working_euclidean_definitionquotient)) -> exists fs_a_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps fs_r_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps fs_s_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_summand. fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps)) * pfc_terms_scale_working_euclidean_definitionquotientstepprevious)) /\ exists fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_summand. pfc_terms_code_working_euclidean_definitionquotientstepprevious = fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps)) * pfc_terms_scale_working_euclidean_definitionquotientstepprevious) + (fs_a_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_partial. fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionquotientstepprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_partial. fs_u_pfc_working_euclidean_definitionquotientstepprevioussum = fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionquotientstepprevioussum) + (fs_r_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_successor. fs_h_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionquotientstepprevioussum)) /\ exists fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_successor. fs_u_pfc_working_euclidean_definitionquotientstepprevioussum = fs_q_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps)) * fs_v_pfc_working_euclidean_definitionquotientstepprevioussum) + (fs_s_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps = fs_r_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps + fs_a_pfc_working_euclidean_definitionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_working_euclidean_definitionquotientsteppreviousresiduebound. pfa_gap_working_euclidean_definitionquotientsteppreviousresiduebound + S (pfd_previous_working_euclidean_definitionquotientstep) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionquotientsteppreviousresiduecongruence pfa_offset_right_working_euclidean_definitionquotientsteppreviousresiduecongruence. (pfc_natural_sum_working_euclidean_definitionquotientstepprevious) + ((p)) * pfa_offset_left_working_euclidean_definitionquotientsteppreviousresiduecongruence = (pfd_previous_working_euclidean_definitionquotientstep) + ((p)) * pfa_offset_right_working_euclidean_definitionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_working_euclidean_definitionquotientstepsubtractleft. pfa_gap_working_euclidean_definitionquotientstepsubtractleft + S (pfd_previous_working_euclidean_definitionquotientstep) = ((p))) /\ (((exists pfa_gap_working_euclidean_definitionquotientstepsubtractright. pfa_gap_working_euclidean_definitionquotientstepsubtractright + S (pfd_difference_working_euclidean_definitionquotientstep) = ((p))) /\ ((((exists pfa_gap_working_euclidean_definitionquotientstepsubtractresultbound. pfa_gap_working_euclidean_definitionquotientstepsubtractresultbound + S (pfd_input_working_euclidean_definitionquotientstep) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionquotientstepsubtractresultcongruence pfa_offset_right_working_euclidean_definitionquotientstepsubtractresultcongruence. ((pfd_previous_working_euclidean_definitionquotientstep) + (pfd_difference_working_euclidean_definitionquotientstep)) + ((p)) * pfa_offset_left_working_euclidean_definitionquotientstepsubtractresultcongruence = (pfd_input_working_euclidean_definitionquotientstep) + ((p)) * pfa_offset_right_working_euclidean_definitionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_working_euclidean_definitionquotientstepmultiplyleft. pfa_gap_working_euclidean_definitionquotientstepmultiplyleft + S (pfd_inverse_working_euclidean_definition) = ((p))) /\ (((exists pfa_gap_working_euclidean_definitionquotientstepmultiplyright. pfa_gap_working_euclidean_definitionquotientstepmultiplyright + S (pfd_difference_working_euclidean_definitionquotientstep) = ((p))) /\ ((((exists pfa_gap_working_euclidean_definitionquotientstepmultiplyresultbound. pfa_gap_working_euclidean_definitionquotientstepmultiplyresultbound + S (pfd_value_working_euclidean_definitionquotient) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionquotientstepmultiplyresultcongruence pfa_offset_right_working_euclidean_definitionquotientstepmultiplyresultcongruence. ((pfd_inverse_working_euclidean_definition) * (pfd_difference_working_euclidean_definitionquotientstep)) + ((p)) * pfa_offset_left_working_euclidean_definitionquotientstepmultiplyresultcongruence = (pfd_value_working_euclidean_definitionquotient) + ((p)) * pfa_offset_right_working_euclidean_definitionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_working_euclidean_definitionproduct. (exists pfa_gap_working_euclidean_definitionproductbound. pfa_gap_working_euclidean_definitionproductbound + S (pfc_index_working_euclidean_definitionproduct) = ((L))) -> exists pfc_value_working_euclidean_definitionproduct. ((((exists ff_h_pfp_working_euclidean_definitionproductentry. ff_h_pfp_working_euclidean_definitionproductentry + S (pfc_value_working_euclidean_definitionproduct) = S ((S (pfc_index_working_euclidean_definitionproduct)) * pfd_product_scale_working_euclidean_definition)) /\ exists ff_q_pfp_working_euclidean_definitionproductentry. pfd_product_code_working_euclidean_definition = ff_q_pfp_working_euclidean_definitionproductentry * S ((S (pfc_index_working_euclidean_definitionproduct)) * pfd_product_scale_working_euclidean_definition) + (pfc_value_working_euclidean_definitionproduct))) /\ ((exists pfc_terms_code_working_euclidean_definitionproductcoefficient pfc_terms_scale_working_euclidean_definitionproductcoefficient pfc_natural_sum_working_euclidean_definitionproductcoefficient. ((forall pfc_index_working_euclidean_definitionproductcoefficientdiagonal. (exists pfa_gap_working_euclidean_definitionproductcoefficientdiagonalbound. pfa_gap_working_euclidean_definitionproductcoefficientdiagonalbound + S (pfc_index_working_euclidean_definitionproductcoefficientdiagonal) = (S (pfc_index_working_euclidean_definitionproduct))) -> exists pfc_value_working_euclidean_definitionproductcoefficientdiagonal. ((((exists ff_h_pfp_working_euclidean_definitionproductcoefficientdiagonalentry. ff_h_pfp_working_euclidean_definitionproductcoefficientdiagonalentry + S (pfc_value_working_euclidean_definitionproductcoefficientdiagonal) = S ((S (pfc_index_working_euclidean_definitionproductcoefficientdiagonal)) * pfc_terms_scale_working_euclidean_definitionproductcoefficient)) /\ exists ff_q_pfp_working_euclidean_definitionproductcoefficientdiagonalentry. pfc_terms_code_working_euclidean_definitionproductcoefficient = ff_q_pfp_working_euclidean_definitionproductcoefficientdiagonalentry * S ((S (pfc_index_working_euclidean_definitionproductcoefficientdiagonal)) * pfc_terms_scale_working_euclidean_definitionproductcoefficient) + (pfc_value_working_euclidean_definitionproductcoefficientdiagonal))) /\ ((exists pfc_complement_working_euclidean_definitionproductcoefficientdiagonalterm pfc_left_working_euclidean_definitionproductcoefficientdiagonalterm pfc_right_working_euclidean_definitionproductcoefficientdiagonalterm. (((pfc_index_working_euclidean_definitionproductcoefficientdiagonal)+pfc_complement_working_euclidean_definitionproductcoefficientdiagonalterm=(pfc_index_working_euclidean_definitionproduct)) /\ ((((((exists pfa_gap_working_euclidean_definitionproductcoefficientdiagonaltermleftinside. pfa_gap_working_euclidean_definitionproductcoefficientdiagonaltermleftinside + S (pfc_index_working_euclidean_definitionproductcoefficientdiagonal) = ((q))) /\ ((((exists ff_h_pfp_working_euclidean_definitionproductcoefficientdiagonaltermleftentry. ff_h_pfp_working_euclidean_definitionproductcoefficientdiagonaltermleftentry + S (pfc_left_working_euclidean_definitionproductcoefficientdiagonalterm) = S ((S (pfc_index_working_euclidean_definitionproductcoefficientdiagonal)) * (qc))) /\ exists ff_q_pfp_working_euclidean_definitionproductcoefficientdiagonaltermleftentry. (qb) = ff_q_pfp_working_euclidean_definitionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_working_euclidean_definitionproductcoefficientdiagonal)) * (qc)) + (pfc_left_working_euclidean_definitionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definitionproductcoefficientdiagonaltermleftoutside. pfc_gap_working_euclidean_definitionproductcoefficientdiagonaltermleftoutside+((q))=(pfc_index_working_euclidean_definitionproductcoefficientdiagonal)) /\ (((pfc_left_working_euclidean_definitionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_working_euclidean_definitionproductcoefficientdiagonaltermrightinside. pfa_gap_working_euclidean_definitionproductcoefficientdiagonaltermrightinside + S (pfc_complement_working_euclidean_definitionproductcoefficientdiagonalterm) = (S ((d)))) /\ ((((exists ff_h_pfp_working_euclidean_definitionproductcoefficientdiagonaltermrightentry. ff_h_pfp_working_euclidean_definitionproductcoefficientdiagonaltermrightentry + S (pfc_right_working_euclidean_definitionproductcoefficientdiagonalterm) = S ((S (pfc_complement_working_euclidean_definitionproductcoefficientdiagonalterm)) * (bc))) /\ exists ff_q_pfp_working_euclidean_definitionproductcoefficientdiagonaltermrightentry. (bb) = ff_q_pfp_working_euclidean_definitionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_working_euclidean_definitionproductcoefficientdiagonalterm)) * (bc)) + (pfc_right_working_euclidean_definitionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definitionproductcoefficientdiagonaltermrightoutside. pfc_gap_working_euclidean_definitionproductcoefficientdiagonaltermrightoutside+(S ((d)))=(pfc_complement_working_euclidean_definitionproductcoefficientdiagonalterm)) /\ (((pfc_right_working_euclidean_definitionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_working_euclidean_definitionproductcoefficientdiagonal)=pfc_left_working_euclidean_definitionproductcoefficientdiagonalterm*pfc_right_working_euclidean_definitionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_working_euclidean_definitionproductcoefficientsum fs_v_pfc_working_euclidean_definitionproductcoefficientsum. ((((exists fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_start. fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_working_euclidean_definitionproductcoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_start. fs_u_pfc_working_euclidean_definitionproductcoefficientsum = fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_working_euclidean_definitionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_terminal. fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_terminal + S (pfc_natural_sum_working_euclidean_definitionproductcoefficient) = S ((S (S (pfc_index_working_euclidean_definitionproduct))) * fs_v_pfc_working_euclidean_definitionproductcoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_terminal. fs_u_pfc_working_euclidean_definitionproductcoefficientsum = fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_working_euclidean_definitionproduct))) * fs_v_pfc_working_euclidean_definitionproductcoefficientsum) + (pfc_natural_sum_working_euclidean_definitionproductcoefficient))) /\ forall fs_i_pfc_working_euclidean_definitionproductcoefficientsum_body_steps. (exists fs_lt_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_bound. fs_lt_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_bound + S fs_i_pfc_working_euclidean_definitionproductcoefficientsum_body_steps = S (pfc_index_working_euclidean_definitionproduct)) -> exists fs_a_pfc_working_euclidean_definitionproductcoefficientsum_body_steps fs_r_pfc_working_euclidean_definitionproductcoefficientsum_body_steps fs_s_pfc_working_euclidean_definitionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_summand. fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_working_euclidean_definitionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definitionproductcoefficientsum_body_steps)) * pfc_terms_scale_working_euclidean_definitionproductcoefficient)) /\ exists fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_summand. pfc_terms_code_working_euclidean_definitionproductcoefficient = fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_working_euclidean_definitionproductcoefficientsum_body_steps)) * pfc_terms_scale_working_euclidean_definitionproductcoefficient) + (fs_a_pfc_working_euclidean_definitionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_partial. fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_working_euclidean_definitionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definitionproductcoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definitionproductcoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_partial. fs_u_pfc_working_euclidean_definitionproductcoefficientsum = fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_working_euclidean_definitionproductcoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definitionproductcoefficientsum) + (fs_r_pfc_working_euclidean_definitionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_successor. fs_h_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_working_euclidean_definitionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_working_euclidean_definitionproductcoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definitionproductcoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_successor. fs_u_pfc_working_euclidean_definitionproductcoefficientsum = fs_q_pfc_working_euclidean_definitionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_working_euclidean_definitionproductcoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definitionproductcoefficientsum) + (fs_s_pfc_working_euclidean_definitionproductcoefficientsum_body_steps))) /\ fs_s_pfc_working_euclidean_definitionproductcoefficientsum_body_steps = fs_r_pfc_working_euclidean_definitionproductcoefficientsum_body_steps + fs_a_pfc_working_euclidean_definitionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_working_euclidean_definitionproductcoefficientresiduebound. pfa_gap_working_euclidean_definitionproductcoefficientresiduebound + S (pfc_value_working_euclidean_definitionproduct) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitionproductcoefficientresiduecongruence pfa_offset_right_working_euclidean_definitionproductcoefficientresiduecongruence. (pfc_natural_sum_working_euclidean_definitionproductcoefficient) + ((p)) * pfa_offset_left_working_euclidean_definitionproductcoefficientresiduecongruence = (pfc_value_working_euclidean_definitionproduct) + ((p)) * pfa_offset_right_working_euclidean_definitionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_working_euclidean_definitiondifference. (exists pfa_gap_working_euclidean_definitiondifferenceindex. pfa_gap_working_euclidean_definitiondifferenceindex + S (pfs_index_working_euclidean_definitiondifference) = ((L))) -> exists pfs_left_working_euclidean_definitiondifference pfs_right_working_euclidean_definitiondifference pfs_result_working_euclidean_definitiondifference. ((((exists ff_h_pfp_working_euclidean_definitiondifferenceleft. ff_h_pfp_working_euclidean_definitiondifferenceleft + S (pfs_left_working_euclidean_definitiondifference) = S ((S (pfs_index_working_euclidean_definitiondifference)) * (ac))) /\ exists ff_q_pfp_working_euclidean_definitiondifferenceleft. (ab) = ff_q_pfp_working_euclidean_definitiondifferenceleft * S ((S (pfs_index_working_euclidean_definitiondifference)) * (ac)) + (pfs_left_working_euclidean_definitiondifference))) /\ (((((exists ff_h_pfp_working_euclidean_definitiondifferenceright. ff_h_pfp_working_euclidean_definitiondifferenceright + S (pfs_right_working_euclidean_definitiondifference) = S ((S (pfs_index_working_euclidean_definitiondifference)) * pfd_product_scale_working_euclidean_definition)) /\ exists ff_q_pfp_working_euclidean_definitiondifferenceright. pfd_product_code_working_euclidean_definition = ff_q_pfp_working_euclidean_definitiondifferenceright * S ((S (pfs_index_working_euclidean_definitiondifference)) * pfd_product_scale_working_euclidean_definition) + (pfs_right_working_euclidean_definitiondifference))) /\ (((((exists ff_h_pfp_working_euclidean_definitiondifferenceresult. ff_h_pfp_working_euclidean_definitiondifferenceresult + S (pfs_result_working_euclidean_definitiondifference) = S ((S (pfs_index_working_euclidean_definitiondifference)) * pfd_residual_scale_working_euclidean_definition)) /\ exists ff_q_pfp_working_euclidean_definitiondifferenceresult. pfd_residual_code_working_euclidean_definition = ff_q_pfp_working_euclidean_definitiondifferenceresult * S ((S (pfs_index_working_euclidean_definitiondifference)) * pfd_residual_scale_working_euclidean_definition) + (pfs_result_working_euclidean_definitiondifference))) /\ ((((exists pfa_gap_working_euclidean_definitiondifferenceoperationleft. pfa_gap_working_euclidean_definitiondifferenceoperationleft + S (pfs_right_working_euclidean_definitiondifference) = ((p))) /\ (((exists pfa_gap_working_euclidean_definitiondifferenceoperationright. pfa_gap_working_euclidean_definitiondifferenceoperationright + S (pfs_result_working_euclidean_definitiondifference) = ((p))) /\ ((((exists pfa_gap_working_euclidean_definitiondifferenceoperationresultbound. pfa_gap_working_euclidean_definitiondifferenceoperationresultbound + S (pfs_left_working_euclidean_definitiondifference) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definitiondifferenceoperationresultcongruence pfa_offset_right_working_euclidean_definitiondifferenceoperationresultcongruence. ((pfs_right_working_euclidean_definitiondifference) + (pfs_result_working_euclidean_definitiondifference)) + ((p)) * pfa_offset_left_working_euclidean_definitiondifferenceoperationresultcongruence = (pfs_left_working_euclidean_definitiondifference) + ((p)) * pfa_offset_right_working_euclidean_definitiondifferenceoperationresultcongruence)))))))))))))))) /\ ((((((L))=(pfd_cut_working_euclidean_definition)+((R))) /\ (((forall fom_index_pfp_working_euclidean_definitiontriminput. (exists fom_gap_pfp_working_euclidean_definitiontriminput_index_bound. fom_gap_pfp_working_euclidean_definitiontriminput_index_bound + S (fom_index_pfp_working_euclidean_definitiontriminput) = (L)) -> exists fom_value_pfp_working_euclidean_definitiontriminput. ((((exists fom_beta_height_pfp_working_euclidean_definitiontriminput_entry. fom_beta_height_pfp_working_euclidean_definitiontriminput_entry + S (fom_value_pfp_working_euclidean_definitiontriminput) = S ((S (fom_index_pfp_working_euclidean_definitiontriminput)) * pfd_residual_scale_working_euclidean_definition)) /\ exists fom_beta_quotient_pfp_working_euclidean_definitiontriminput_entry. pfd_residual_code_working_euclidean_definition = fom_beta_quotient_pfp_working_euclidean_definitiontriminput_entry * S ((S (fom_index_pfp_working_euclidean_definitiontriminput)) * pfd_residual_scale_working_euclidean_definition) + (fom_value_pfp_working_euclidean_definitiontriminput))) /\ (exists fom_gap_pfp_working_euclidean_definitiontriminput_value_bound. fom_gap_pfp_working_euclidean_definitiontriminput_value_bound + S (fom_value_pfp_working_euclidean_definitiontriminput) = (p)))) /\ (((forall pfp_repeat_index_working_euclidean_definitiontrimremoved. (exists pfa_gap_working_euclidean_definitiontrimremovedindex. pfa_gap_working_euclidean_definitiontrimremovedindex + S (pfp_repeat_index_working_euclidean_definitiontrimremoved) = (pfd_cut_working_euclidean_definition)) -> (((exists ff_h_pfp_working_euclidean_definitiontrimremovedentry. ff_h_pfp_working_euclidean_definitiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_working_euclidean_definitiontrimremoved)) * pfd_residual_scale_working_euclidean_definition)) /\ exists ff_q_pfp_working_euclidean_definitiontrimremovedentry. pfd_residual_code_working_euclidean_definition = ff_q_pfp_working_euclidean_definitiontrimremovedentry * S ((S (pfp_repeat_index_working_euclidean_definitiontrimremoved)) * pfd_residual_scale_working_euclidean_definition) + (0)))) /\ (((forall pftrim_index_working_euclidean_definitiontrimsuffix pftrim_value_working_euclidean_definitiontrimsuffix. (exists pfa_gap_working_euclidean_definitiontrimsuffixbound. pfa_gap_working_euclidean_definitiontrimsuffixbound + S (pftrim_index_working_euclidean_definitiontrimsuffix) = ((R))) -> (((exists ff_h_pfp_working_euclidean_definitiontrimsuffixsource. ff_h_pfp_working_euclidean_definitiontrimsuffixsource + S (pftrim_value_working_euclidean_definitiontrimsuffix) = S ((S ((pfd_cut_working_euclidean_definition)+pftrim_index_working_euclidean_definitiontrimsuffix)) * pfd_residual_scale_working_euclidean_definition)) /\ exists ff_q_pfp_working_euclidean_definitiontrimsuffixsource. pfd_residual_code_working_euclidean_definition = ff_q_pfp_working_euclidean_definitiontrimsuffixsource * S ((S ((pfd_cut_working_euclidean_definition)+pftrim_index_working_euclidean_definitiontrimsuffix)) * pfd_residual_scale_working_euclidean_definition) + (pftrim_value_working_euclidean_definitiontrimsuffix))) -> (((exists ff_h_pfp_working_euclidean_definitiontrimsuffixoutput. ff_h_pfp_working_euclidean_definitiontrimsuffixoutput + S (pftrim_value_working_euclidean_definitiontrimsuffix) = S ((S (pftrim_index_working_euclidean_definitiontrimsuffix)) * (rc))) /\ exists ff_q_pfp_working_euclidean_definitiontrimsuffixoutput. (rb) = ff_q_pfp_working_euclidean_definitiontrimsuffixoutput * S ((S (pftrim_index_working_euclidean_definitiontrimsuffix)) * (rc)) + (pftrim_value_working_euclidean_definitiontrimsuffix)))) /\ ((((R))=0 \/ (exists pftrim_leading_working_euclidean_definitiontrimnormal. ((((exists ff_h_pfp_working_euclidean_definitiontrimnormalentry. ff_h_pfp_working_euclidean_definitiontrimnormalentry + S (pftrim_leading_working_euclidean_definitiontrimnormal) = S ((S (0)) * (rc))) /\ exists ff_q_pfp_working_euclidean_definitiontrimnormalentry. (rb) = ff_q_pfp_working_euclidean_definitiontrimnormalentry * S ((S (0)) * (rc)) + (pftrim_leading_working_euclidean_definitiontrimnormal))) /\ ((~(pftrim_leading_working_euclidean_definitiontrimnormal=0))))))))))))))))))))))))))))))))

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