FpPolynomialCommonRightDivisor(p,db,dc,D,ab,ac,L,bb,bc,M)

((((forall fom_index_pfp_working_euclidean_definition_left_canonical. (exists fom_gap_pfp_working_euclidean_definition_left_canonical_index_bound. fom_gap_pfp_working_euclidean_definition_left_canonical_index_bound + S (fom_index_pfp_working_euclidean_definition_left_canonical) = (L)) -> exists fom_value_pfp_working_euclidean_definition_left_canonical. ((((exists fom_beta_height_pfp_working_euclidean_definition_left_canonical_entry. fom_beta_height_pfp_working_euclidean_definition_left_canonical_entry + S (fom_value_pfp_working_euclidean_definition_left_canonical) = S ((S (fom_index_pfp_working_euclidean_definition_left_canonical)) * (ac))) /\ exists fom_beta_quotient_pfp_working_euclidean_definition_left_canonical_entry. (ab) = fom_beta_quotient_pfp_working_euclidean_definition_left_canonical_entry * S ((S (fom_index_pfp_working_euclidean_definition_left_canonical)) * (ac)) + (fom_value_pfp_working_euclidean_definition_left_canonical))) /\ (exists fom_gap_pfp_working_euclidean_definition_left_canonical_value_bound. fom_gap_pfp_working_euclidean_definition_left_canonical_value_bound + S (fom_value_pfp_working_euclidean_definition_left_canonical) = (p)))) /\ ((exists pfrd_qb_working_euclidean_definition_left pfrd_qc_working_euclidean_definition_left pfrd_qlen_working_euclidean_definition_left pfrd_pb_working_euclidean_definition_left pfrd_pc_working_euclidean_definition_left pfrd_plen_working_euclidean_definition_left. ((((forall fom_index_pfp_working_euclidean_definition_left_productleft. (exists fom_gap_pfp_working_euclidean_definition_left_productleft_index_bound. fom_gap_pfp_working_euclidean_definition_left_productleft_index_bound + S (fom_index_pfp_working_euclidean_definition_left_productleft) = pfrd_qlen_working_euclidean_definition_left) -> exists fom_value_pfp_working_euclidean_definition_left_productleft. ((((exists fom_beta_height_pfp_working_euclidean_definition_left_productleft_entry. fom_beta_height_pfp_working_euclidean_definition_left_productleft_entry + S (fom_value_pfp_working_euclidean_definition_left_productleft) = S ((S (fom_index_pfp_working_euclidean_definition_left_productleft)) * pfrd_qc_working_euclidean_definition_left)) /\ exists fom_beta_quotient_pfp_working_euclidean_definition_left_productleft_entry. pfrd_qb_working_euclidean_definition_left = fom_beta_quotient_pfp_working_euclidean_definition_left_productleft_entry * S ((S (fom_index_pfp_working_euclidean_definition_left_productleft)) * pfrd_qc_working_euclidean_definition_left) + (fom_value_pfp_working_euclidean_definition_left_productleft))) /\ (exists fom_gap_pfp_working_euclidean_definition_left_productleft_value_bound. fom_gap_pfp_working_euclidean_definition_left_productleft_value_bound + S (fom_value_pfp_working_euclidean_definition_left_productleft) = (p)))) /\ (((forall fom_index_pfp_working_euclidean_definition_left_productright. (exists fom_gap_pfp_working_euclidean_definition_left_productright_index_bound. fom_gap_pfp_working_euclidean_definition_left_productright_index_bound + S (fom_index_pfp_working_euclidean_definition_left_productright) = (D)) -> exists fom_value_pfp_working_euclidean_definition_left_productright. ((((exists fom_beta_height_pfp_working_euclidean_definition_left_productright_entry. fom_beta_height_pfp_working_euclidean_definition_left_productright_entry + S (fom_value_pfp_working_euclidean_definition_left_productright) = S ((S (fom_index_pfp_working_euclidean_definition_left_productright)) * (dc))) /\ exists fom_beta_quotient_pfp_working_euclidean_definition_left_productright_entry. (db) = fom_beta_quotient_pfp_working_euclidean_definition_left_productright_entry * S ((S (fom_index_pfp_working_euclidean_definition_left_productright)) * (dc)) + (fom_value_pfp_working_euclidean_definition_left_productright))) /\ (exists fom_gap_pfp_working_euclidean_definition_left_productright_value_bound. fom_gap_pfp_working_euclidean_definition_left_productright_value_bound + S (fom_value_pfp_working_euclidean_definition_left_productright) = (p)))) /\ (((((((pfrd_qlen_working_euclidean_definition_left)=0 \/ ((D))=0) /\ (((pfrd_plen_working_euclidean_definition_left)=0)))) \/ (((~((pfrd_qlen_working_euclidean_definition_left)=0)) /\ (((~(((D))=0)) /\ (((pfrd_qlen_working_euclidean_definition_left)+((D))=S (pfrd_plen_working_euclidean_definition_left)))))))) /\ ((forall pfc_index_working_euclidean_definition_left_productcoefficients. (exists pfa_gap_working_euclidean_definition_left_productcoefficientsbound. pfa_gap_working_euclidean_definition_left_productcoefficientsbound + S (pfc_index_working_euclidean_definition_left_productcoefficients) = (pfrd_plen_working_euclidean_definition_left)) -> exists pfc_value_working_euclidean_definition_left_productcoefficients. ((((exists ff_h_pfp_working_euclidean_definition_left_productcoefficientsentry. ff_h_pfp_working_euclidean_definition_left_productcoefficientsentry + S (pfc_value_working_euclidean_definition_left_productcoefficients) = S ((S (pfc_index_working_euclidean_definition_left_productcoefficients)) * pfrd_pc_working_euclidean_definition_left)) /\ exists ff_q_pfp_working_euclidean_definition_left_productcoefficientsentry. pfrd_pb_working_euclidean_definition_left = ff_q_pfp_working_euclidean_definition_left_productcoefficientsentry * S ((S (pfc_index_working_euclidean_definition_left_productcoefficients)) * pfrd_pc_working_euclidean_definition_left) + (pfc_value_working_euclidean_definition_left_productcoefficients))) /\ ((exists pfc_terms_code_working_euclidean_definition_left_productcoefficientscoefficient pfc_terms_scale_working_euclidean_definition_left_productcoefficientscoefficient pfc_natural_sum_working_euclidean_definition_left_productcoefficientscoefficient. ((forall pfc_index_working_euclidean_definition_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonalbound. pfa_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_working_euclidean_definition_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_working_euclidean_definition_left_productcoefficients))) -> exists pfc_value_working_euclidean_definition_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_working_euclidean_definition_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_working_euclidean_definition_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_working_euclidean_definition_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_working_euclidean_definition_left_productcoefficientscoefficient = ff_q_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_working_euclidean_definition_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_working_euclidean_definition_left_productcoefficientscoefficient) + (pfc_value_working_euclidean_definition_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm pfc_left_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm pfc_right_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_working_euclidean_definition_left_productcoefficientscoefficientdiagonal)+pfc_complement_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm=(pfc_index_working_euclidean_definition_left_productcoefficients)) /\ ((((((exists pfa_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_working_euclidean_definition_left_productcoefficientscoefficientdiagonal) = (pfrd_qlen_working_euclidean_definition_left)) /\ ((((exists ff_h_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_working_euclidean_definition_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_working_euclidean_definition_left)) /\ exists ff_q_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_working_euclidean_definition_left = ff_q_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_working_euclidean_definition_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_working_euclidean_definition_left) + (pfc_left_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_working_euclidean_definition_left)=(pfc_index_working_euclidean_definition_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm) = ((D))) /\ ((((exists ff_h_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm)) * (dc))) /\ exists ff_q_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermrightentry. (db) = ff_q_pfp_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm)) * (dc)) + (pfc_right_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_working_euclidean_definition_left_productcoefficientscoefficientdiagonaltermrightoutside+((D))=(pfc_complement_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_working_euclidean_definition_left_productcoefficientscoefficientdiagonal)=pfc_left_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm*pfc_right_working_euclidean_definition_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum fs_v_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum = fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_working_euclidean_definition_left_productcoefficientscoefficient) = S ((S (S (pfc_index_working_euclidean_definition_left_productcoefficients))) * fs_v_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum = fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_working_euclidean_definition_left_productcoefficients))) * fs_v_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum) + (pfc_natural_sum_working_euclidean_definition_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_working_euclidean_definition_left_productcoefficients)) -> exists fs_a_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_working_euclidean_definition_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_working_euclidean_definition_left_productcoefficientscoefficient = fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_working_euclidean_definition_left_productcoefficientscoefficient) + (fs_a_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum = fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum) + (fs_r_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum = fs_q_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum) + (fs_s_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_working_euclidean_definition_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_working_euclidean_definition_left_productcoefficientscoefficientresiduebound. pfa_gap_working_euclidean_definition_left_productcoefficientscoefficientresiduebound + S (pfc_value_working_euclidean_definition_left_productcoefficients) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definition_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_working_euclidean_definition_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_working_euclidean_definition_left_productcoefficientscoefficient) + ((p)) * pfa_offset_left_working_euclidean_definition_left_productcoefficientscoefficientresiduecongruence = (pfc_value_working_euclidean_definition_left_productcoefficients) + ((p)) * pfa_offset_right_working_euclidean_definition_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_working_euclidean_definition_left_target pfrep_left_working_euclidean_definition_left_target pfrep_right_working_euclidean_definition_left_target. ((exists pfrep_position_working_euclidean_definition_left_targetfirst. ((pfrep_position_working_euclidean_definition_left_targetfirst+S (pfrep_power_working_euclidean_definition_left_target)=(pfrd_plen_working_euclidean_definition_left)) /\ ((((exists ff_h_pfp_working_euclidean_definition_left_targetfirstentry. ff_h_pfp_working_euclidean_definition_left_targetfirstentry + S (pfrep_left_working_euclidean_definition_left_target) = S ((S (pfrep_position_working_euclidean_definition_left_targetfirst)) * pfrd_pc_working_euclidean_definition_left)) /\ exists ff_q_pfp_working_euclidean_definition_left_targetfirstentry. pfrd_pb_working_euclidean_definition_left = ff_q_pfp_working_euclidean_definition_left_targetfirstentry * S ((S (pfrep_position_working_euclidean_definition_left_targetfirst)) * pfrd_pc_working_euclidean_definition_left) + (pfrep_left_working_euclidean_definition_left_target)))))) \/ (((exists pfrep_gap_working_euclidean_definition_left_targetfirstoutside. pfrep_gap_working_euclidean_definition_left_targetfirstoutside+(pfrd_plen_working_euclidean_definition_left)=(pfrep_power_working_euclidean_definition_left_target)) /\ (((pfrep_left_working_euclidean_definition_left_target)=0))))) -> ((exists pfrep_position_working_euclidean_definition_left_targetsecond. ((pfrep_position_working_euclidean_definition_left_targetsecond+S (pfrep_power_working_euclidean_definition_left_target)=((L))) /\ ((((exists ff_h_pfp_working_euclidean_definition_left_targetsecondentry. ff_h_pfp_working_euclidean_definition_left_targetsecondentry + S (pfrep_right_working_euclidean_definition_left_target) = S ((S (pfrep_position_working_euclidean_definition_left_targetsecond)) * (ac))) /\ exists ff_q_pfp_working_euclidean_definition_left_targetsecondentry. (ab) = ff_q_pfp_working_euclidean_definition_left_targetsecondentry * S ((S (pfrep_position_working_euclidean_definition_left_targetsecond)) * (ac)) + (pfrep_right_working_euclidean_definition_left_target)))))) \/ (((exists pfrep_gap_working_euclidean_definition_left_targetsecondoutside. pfrep_gap_working_euclidean_definition_left_targetsecondoutside+((L))=(pfrep_power_working_euclidean_definition_left_target)) /\ (((pfrep_right_working_euclidean_definition_left_target)=0))))) -> pfrep_left_working_euclidean_definition_left_target=pfrep_right_working_euclidean_definition_left_target))))))) /\ ((((forall fom_index_pfp_working_euclidean_definition_right_canonical. (exists fom_gap_pfp_working_euclidean_definition_right_canonical_index_bound. fom_gap_pfp_working_euclidean_definition_right_canonical_index_bound + S (fom_index_pfp_working_euclidean_definition_right_canonical) = (M)) -> exists fom_value_pfp_working_euclidean_definition_right_canonical. ((((exists fom_beta_height_pfp_working_euclidean_definition_right_canonical_entry. fom_beta_height_pfp_working_euclidean_definition_right_canonical_entry + S (fom_value_pfp_working_euclidean_definition_right_canonical) = S ((S (fom_index_pfp_working_euclidean_definition_right_canonical)) * (bc))) /\ exists fom_beta_quotient_pfp_working_euclidean_definition_right_canonical_entry. (bb) = fom_beta_quotient_pfp_working_euclidean_definition_right_canonical_entry * S ((S (fom_index_pfp_working_euclidean_definition_right_canonical)) * (bc)) + (fom_value_pfp_working_euclidean_definition_right_canonical))) /\ (exists fom_gap_pfp_working_euclidean_definition_right_canonical_value_bound. fom_gap_pfp_working_euclidean_definition_right_canonical_value_bound + S (fom_value_pfp_working_euclidean_definition_right_canonical) = (p)))) /\ ((exists pfrd_qb_working_euclidean_definition_right pfrd_qc_working_euclidean_definition_right pfrd_qlen_working_euclidean_definition_right pfrd_pb_working_euclidean_definition_right pfrd_pc_working_euclidean_definition_right pfrd_plen_working_euclidean_definition_right. ((((forall fom_index_pfp_working_euclidean_definition_right_productleft. (exists fom_gap_pfp_working_euclidean_definition_right_productleft_index_bound. fom_gap_pfp_working_euclidean_definition_right_productleft_index_bound + S (fom_index_pfp_working_euclidean_definition_right_productleft) = pfrd_qlen_working_euclidean_definition_right) -> exists fom_value_pfp_working_euclidean_definition_right_productleft. ((((exists fom_beta_height_pfp_working_euclidean_definition_right_productleft_entry. fom_beta_height_pfp_working_euclidean_definition_right_productleft_entry + S (fom_value_pfp_working_euclidean_definition_right_productleft) = S ((S (fom_index_pfp_working_euclidean_definition_right_productleft)) * pfrd_qc_working_euclidean_definition_right)) /\ exists fom_beta_quotient_pfp_working_euclidean_definition_right_productleft_entry. pfrd_qb_working_euclidean_definition_right = fom_beta_quotient_pfp_working_euclidean_definition_right_productleft_entry * S ((S (fom_index_pfp_working_euclidean_definition_right_productleft)) * pfrd_qc_working_euclidean_definition_right) + (fom_value_pfp_working_euclidean_definition_right_productleft))) /\ (exists fom_gap_pfp_working_euclidean_definition_right_productleft_value_bound. fom_gap_pfp_working_euclidean_definition_right_productleft_value_bound + S (fom_value_pfp_working_euclidean_definition_right_productleft) = (p)))) /\ (((forall fom_index_pfp_working_euclidean_definition_right_productright. (exists fom_gap_pfp_working_euclidean_definition_right_productright_index_bound. fom_gap_pfp_working_euclidean_definition_right_productright_index_bound + S (fom_index_pfp_working_euclidean_definition_right_productright) = (D)) -> exists fom_value_pfp_working_euclidean_definition_right_productright. ((((exists fom_beta_height_pfp_working_euclidean_definition_right_productright_entry. fom_beta_height_pfp_working_euclidean_definition_right_productright_entry + S (fom_value_pfp_working_euclidean_definition_right_productright) = S ((S (fom_index_pfp_working_euclidean_definition_right_productright)) * (dc))) /\ exists fom_beta_quotient_pfp_working_euclidean_definition_right_productright_entry. (db) = fom_beta_quotient_pfp_working_euclidean_definition_right_productright_entry * S ((S (fom_index_pfp_working_euclidean_definition_right_productright)) * (dc)) + (fom_value_pfp_working_euclidean_definition_right_productright))) /\ (exists fom_gap_pfp_working_euclidean_definition_right_productright_value_bound. fom_gap_pfp_working_euclidean_definition_right_productright_value_bound + S (fom_value_pfp_working_euclidean_definition_right_productright) = (p)))) /\ (((((((pfrd_qlen_working_euclidean_definition_right)=0 \/ ((D))=0) /\ (((pfrd_plen_working_euclidean_definition_right)=0)))) \/ (((~((pfrd_qlen_working_euclidean_definition_right)=0)) /\ (((~(((D))=0)) /\ (((pfrd_qlen_working_euclidean_definition_right)+((D))=S (pfrd_plen_working_euclidean_definition_right)))))))) /\ ((forall pfc_index_working_euclidean_definition_right_productcoefficients. (exists pfa_gap_working_euclidean_definition_right_productcoefficientsbound. pfa_gap_working_euclidean_definition_right_productcoefficientsbound + S (pfc_index_working_euclidean_definition_right_productcoefficients) = (pfrd_plen_working_euclidean_definition_right)) -> exists pfc_value_working_euclidean_definition_right_productcoefficients. ((((exists ff_h_pfp_working_euclidean_definition_right_productcoefficientsentry. ff_h_pfp_working_euclidean_definition_right_productcoefficientsentry + S (pfc_value_working_euclidean_definition_right_productcoefficients) = S ((S (pfc_index_working_euclidean_definition_right_productcoefficients)) * pfrd_pc_working_euclidean_definition_right)) /\ exists ff_q_pfp_working_euclidean_definition_right_productcoefficientsentry. pfrd_pb_working_euclidean_definition_right = ff_q_pfp_working_euclidean_definition_right_productcoefficientsentry * S ((S (pfc_index_working_euclidean_definition_right_productcoefficients)) * pfrd_pc_working_euclidean_definition_right) + (pfc_value_working_euclidean_definition_right_productcoefficients))) /\ ((exists pfc_terms_code_working_euclidean_definition_right_productcoefficientscoefficient pfc_terms_scale_working_euclidean_definition_right_productcoefficientscoefficient pfc_natural_sum_working_euclidean_definition_right_productcoefficientscoefficient. ((forall pfc_index_working_euclidean_definition_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonalbound. pfa_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_working_euclidean_definition_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_working_euclidean_definition_right_productcoefficients))) -> exists pfc_value_working_euclidean_definition_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_working_euclidean_definition_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_working_euclidean_definition_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_working_euclidean_definition_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_working_euclidean_definition_right_productcoefficientscoefficient = ff_q_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_working_euclidean_definition_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_working_euclidean_definition_right_productcoefficientscoefficient) + (pfc_value_working_euclidean_definition_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm pfc_left_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm pfc_right_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_working_euclidean_definition_right_productcoefficientscoefficientdiagonal)+pfc_complement_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm=(pfc_index_working_euclidean_definition_right_productcoefficients)) /\ ((((((exists pfa_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_working_euclidean_definition_right_productcoefficientscoefficientdiagonal) = (pfrd_qlen_working_euclidean_definition_right)) /\ ((((exists ff_h_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_working_euclidean_definition_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_working_euclidean_definition_right)) /\ exists ff_q_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_working_euclidean_definition_right = ff_q_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_working_euclidean_definition_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_working_euclidean_definition_right) + (pfc_left_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_working_euclidean_definition_right)=(pfc_index_working_euclidean_definition_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm) = ((D))) /\ ((((exists ff_h_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm)) * (dc))) /\ exists ff_q_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermrightentry. (db) = ff_q_pfp_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm)) * (dc)) + (pfc_right_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_working_euclidean_definition_right_productcoefficientscoefficientdiagonaltermrightoutside+((D))=(pfc_complement_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_working_euclidean_definition_right_productcoefficientscoefficientdiagonal)=pfc_left_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm*pfc_right_working_euclidean_definition_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum fs_v_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum = fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_working_euclidean_definition_right_productcoefficientscoefficient) = S ((S (S (pfc_index_working_euclidean_definition_right_productcoefficients))) * fs_v_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum = fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_working_euclidean_definition_right_productcoefficients))) * fs_v_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum) + (pfc_natural_sum_working_euclidean_definition_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_working_euclidean_definition_right_productcoefficients)) -> exists fs_a_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_working_euclidean_definition_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_working_euclidean_definition_right_productcoefficientscoefficient = fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_working_euclidean_definition_right_productcoefficientscoefficient) + (fs_a_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum = fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum) + (fs_r_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum = fs_q_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum) + (fs_s_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_working_euclidean_definition_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_working_euclidean_definition_right_productcoefficientscoefficientresiduebound. pfa_gap_working_euclidean_definition_right_productcoefficientscoefficientresiduebound + S (pfc_value_working_euclidean_definition_right_productcoefficients) = ((p))) /\ ((exists pfa_offset_left_working_euclidean_definition_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_working_euclidean_definition_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_working_euclidean_definition_right_productcoefficientscoefficient) + ((p)) * pfa_offset_left_working_euclidean_definition_right_productcoefficientscoefficientresiduecongruence = (pfc_value_working_euclidean_definition_right_productcoefficients) + ((p)) * pfa_offset_right_working_euclidean_definition_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_working_euclidean_definition_right_target pfrep_left_working_euclidean_definition_right_target pfrep_right_working_euclidean_definition_right_target. ((exists pfrep_position_working_euclidean_definition_right_targetfirst. ((pfrep_position_working_euclidean_definition_right_targetfirst+S (pfrep_power_working_euclidean_definition_right_target)=(pfrd_plen_working_euclidean_definition_right)) /\ ((((exists ff_h_pfp_working_euclidean_definition_right_targetfirstentry. ff_h_pfp_working_euclidean_definition_right_targetfirstentry + S (pfrep_left_working_euclidean_definition_right_target) = S ((S (pfrep_position_working_euclidean_definition_right_targetfirst)) * pfrd_pc_working_euclidean_definition_right)) /\ exists ff_q_pfp_working_euclidean_definition_right_targetfirstentry. pfrd_pb_working_euclidean_definition_right = ff_q_pfp_working_euclidean_definition_right_targetfirstentry * S ((S (pfrep_position_working_euclidean_definition_right_targetfirst)) * pfrd_pc_working_euclidean_definition_right) + (pfrep_left_working_euclidean_definition_right_target)))))) \/ (((exists pfrep_gap_working_euclidean_definition_right_targetfirstoutside. pfrep_gap_working_euclidean_definition_right_targetfirstoutside+(pfrd_plen_working_euclidean_definition_right)=(pfrep_power_working_euclidean_definition_right_target)) /\ (((pfrep_left_working_euclidean_definition_right_target)=0))))) -> ((exists pfrep_position_working_euclidean_definition_right_targetsecond. ((pfrep_position_working_euclidean_definition_right_targetsecond+S (pfrep_power_working_euclidean_definition_right_target)=((M))) /\ ((((exists ff_h_pfp_working_euclidean_definition_right_targetsecondentry. ff_h_pfp_working_euclidean_definition_right_targetsecondentry + S (pfrep_right_working_euclidean_definition_right_target) = S ((S (pfrep_position_working_euclidean_definition_right_targetsecond)) * (bc))) /\ exists ff_q_pfp_working_euclidean_definition_right_targetsecondentry. (bb) = ff_q_pfp_working_euclidean_definition_right_targetsecondentry * S ((S (pfrep_position_working_euclidean_definition_right_targetsecond)) * (bc)) + (pfrep_right_working_euclidean_definition_right_target)))))) \/ (((exists pfrep_gap_working_euclidean_definition_right_targetsecondoutside. pfrep_gap_working_euclidean_definition_right_targetsecondoutside+((M))=(pfrep_power_working_euclidean_definition_right_target)) /\ (((pfrep_right_working_euclidean_definition_right_target)=0))))) -> pfrep_left_working_euclidean_definition_right_target=pfrep_right_working_euclidean_definition_right_target)))))))))

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