FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)

((forall fom_index_pfp_lowercontinuationleft. (exists fom_gap_pfp_lowercontinuationleft_index_bound. fom_gap_pfp_lowercontinuationleft_index_bound + S (fom_index_pfp_lowercontinuationleft) = (L)) -> exists fom_value_pfp_lowercontinuationleft. ((((exists fom_beta_height_pfp_lowercontinuationleft_entry. fom_beta_height_pfp_lowercontinuationleft_entry + S (fom_value_pfp_lowercontinuationleft) = S ((S (fom_index_pfp_lowercontinuationleft)) * (ac))) /\ exists fom_beta_quotient_pfp_lowercontinuationleft_entry. (ab) = fom_beta_quotient_pfp_lowercontinuationleft_entry * S ((S (fom_index_pfp_lowercontinuationleft)) * (ac)) + (fom_value_pfp_lowercontinuationleft))) /\ (exists fom_gap_pfp_lowercontinuationleft_value_bound. fom_gap_pfp_lowercontinuationleft_value_bound + S (fom_value_pfp_lowercontinuationleft) = (p)))) /\ (((forall fom_index_pfp_lowercontinuationright. (exists fom_gap_pfp_lowercontinuationright_index_bound. fom_gap_pfp_lowercontinuationright_index_bound + S (fom_index_pfp_lowercontinuationright) = (M)) -> exists fom_value_pfp_lowercontinuationright. ((((exists fom_beta_height_pfp_lowercontinuationright_entry. fom_beta_height_pfp_lowercontinuationright_entry + S (fom_value_pfp_lowercontinuationright) = S ((S (fom_index_pfp_lowercontinuationright)) * (bc))) /\ exists fom_beta_quotient_pfp_lowercontinuationright_entry. (bb) = fom_beta_quotient_pfp_lowercontinuationright_entry * S ((S (fom_index_pfp_lowercontinuationright)) * (bc)) + (fom_value_pfp_lowercontinuationright))) /\ (exists fom_gap_pfp_lowercontinuationright_value_bound. fom_gap_pfp_lowercontinuationright_value_bound + S (fom_value_pfp_lowercontinuationright) = (p)))) /\ ((((((((L))=0 \/ ((M))=0) /\ ((((N))=0)))) \/ (((~(((L))=0)) /\ (((~(((M))=0)) /\ ((((L))+((M))=S ((N))))))))) /\ ((forall pfc_index_lowercontinuationcoefficients. (exists pfa_gap_lowercontinuationcoefficientsbound. pfa_gap_lowercontinuationcoefficientsbound + S (pfc_index_lowercontinuationcoefficients) = ((N))) -> exists pfc_value_lowercontinuationcoefficients. ((((exists ff_h_pfp_lowercontinuationcoefficientsentry. ff_h_pfp_lowercontinuationcoefficientsentry + S (pfc_value_lowercontinuationcoefficients) = S ((S (pfc_index_lowercontinuationcoefficients)) * (cc))) /\ exists ff_q_pfp_lowercontinuationcoefficientsentry. (cb) = ff_q_pfp_lowercontinuationcoefficientsentry * S ((S (pfc_index_lowercontinuationcoefficients)) * (cc)) + (pfc_value_lowercontinuationcoefficients))) /\ ((exists pfc_terms_code_lowercontinuationcoefficientscoefficient pfc_terms_scale_lowercontinuationcoefficientscoefficient pfc_natural_sum_lowercontinuationcoefficientscoefficient. ((forall pfc_index_lowercontinuationcoefficientscoefficientdiagonal. (exists pfa_gap_lowercontinuationcoefficientscoefficientdiagonalbound. pfa_gap_lowercontinuationcoefficientscoefficientdiagonalbound + S (pfc_index_lowercontinuationcoefficientscoefficientdiagonal) = (S (pfc_index_lowercontinuationcoefficients))) -> exists pfc_value_lowercontinuationcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_lowercontinuationcoefficientscoefficientdiagonalentry. ff_h_pfp_lowercontinuationcoefficientscoefficientdiagonalentry + S (pfc_value_lowercontinuationcoefficientscoefficientdiagonal) = S ((S (pfc_index_lowercontinuationcoefficientscoefficientdiagonal)) * pfc_terms_scale_lowercontinuationcoefficientscoefficient)) /\ exists ff_q_pfp_lowercontinuationcoefficientscoefficientdiagonalentry. pfc_terms_code_lowercontinuationcoefficientscoefficient = ff_q_pfp_lowercontinuationcoefficientscoefficientdiagonalentry * S ((S (pfc_index_lowercontinuationcoefficientscoefficientdiagonal)) * pfc_terms_scale_lowercontinuationcoefficientscoefficient) + (pfc_value_lowercontinuationcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_lowercontinuationcoefficientscoefficientdiagonalterm pfc_left_lowercontinuationcoefficientscoefficientdiagonalterm pfc_right_lowercontinuationcoefficientscoefficientdiagonalterm. (((pfc_index_lowercontinuationcoefficientscoefficientdiagonal)+pfc_complement_lowercontinuationcoefficientscoefficientdiagonalterm=(pfc_index_lowercontinuationcoefficients)) /\ ((((((exists pfa_gap_lowercontinuationcoefficientscoefficientdiagonaltermleftinside. pfa_gap_lowercontinuationcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_lowercontinuationcoefficientscoefficientdiagonal) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_lowercontinuationcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_lowercontinuationcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_lowercontinuationcoefficientscoefficientdiagonal)) * (ac))) /\ exists ff_q_pfp_lowercontinuationcoefficientscoefficientdiagonaltermleftentry. (ab) = ff_q_pfp_lowercontinuationcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_lowercontinuationcoefficientscoefficientdiagonal)) * (ac)) + (pfc_left_lowercontinuationcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_lowercontinuationcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_lowercontinuationcoefficientscoefficientdiagonaltermleftoutside+((L))=(pfc_index_lowercontinuationcoefficientscoefficientdiagonal)) /\ (((pfc_left_lowercontinuationcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_lowercontinuationcoefficientscoefficientdiagonaltermrightinside. pfa_gap_lowercontinuationcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_lowercontinuationcoefficientscoefficientdiagonalterm) = ((M))) /\ ((((exists ff_h_pfp_lowercontinuationcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_lowercontinuationcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_lowercontinuationcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_lowercontinuationcoefficientscoefficientdiagonalterm)) * (bc))) /\ exists ff_q_pfp_lowercontinuationcoefficientscoefficientdiagonaltermrightentry. (bb) = ff_q_pfp_lowercontinuationcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_lowercontinuationcoefficientscoefficientdiagonalterm)) * (bc)) + (pfc_right_lowercontinuationcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_lowercontinuationcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_lowercontinuationcoefficientscoefficientdiagonaltermrightoutside+((M))=(pfc_complement_lowercontinuationcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_lowercontinuationcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_lowercontinuationcoefficientscoefficientdiagonal)=pfc_left_lowercontinuationcoefficientscoefficientdiagonalterm*pfc_right_lowercontinuationcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_lowercontinuationcoefficientscoefficientsum fs_v_pfc_lowercontinuationcoefficientscoefficientsum. ((((exists fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_start. fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_lowercontinuationcoefficientscoefficientsum)) /\ exists fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_start. fs_u_pfc_lowercontinuationcoefficientscoefficientsum = fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_lowercontinuationcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_terminal. fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_lowercontinuationcoefficientscoefficient) = S ((S (S (pfc_index_lowercontinuationcoefficients))) * fs_v_pfc_lowercontinuationcoefficientscoefficientsum)) /\ exists fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_terminal. fs_u_pfc_lowercontinuationcoefficientscoefficientsum = fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_lowercontinuationcoefficients))) * fs_v_pfc_lowercontinuationcoefficientscoefficientsum) + (pfc_natural_sum_lowercontinuationcoefficientscoefficient))) /\ forall fs_i_pfc_lowercontinuationcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_lowercontinuationcoefficientscoefficientsum_body_steps = S (pfc_index_lowercontinuationcoefficients)) -> exists fs_a_pfc_lowercontinuationcoefficientscoefficientsum_body_steps fs_r_pfc_lowercontinuationcoefficientscoefficientsum_body_steps fs_s_pfc_lowercontinuationcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_lowercontinuationcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_lowercontinuationcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_lowercontinuationcoefficientscoefficient)) /\ exists fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_lowercontinuationcoefficientscoefficient = fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_lowercontinuationcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_lowercontinuationcoefficientscoefficient) + (fs_a_pfc_lowercontinuationcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_lowercontinuationcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_lowercontinuationcoefficientscoefficientsum_body_steps)) * fs_v_pfc_lowercontinuationcoefficientscoefficientsum)) /\ exists fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_lowercontinuationcoefficientscoefficientsum = fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_lowercontinuationcoefficientscoefficientsum_body_steps)) * fs_v_pfc_lowercontinuationcoefficientscoefficientsum) + (fs_r_pfc_lowercontinuationcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_lowercontinuationcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_lowercontinuationcoefficientscoefficientsum_body_steps)) * fs_v_pfc_lowercontinuationcoefficientscoefficientsum)) /\ exists fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_lowercontinuationcoefficientscoefficientsum = fs_q_pfc_lowercontinuationcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_lowercontinuationcoefficientscoefficientsum_body_steps)) * fs_v_pfc_lowercontinuationcoefficientscoefficientsum) + (fs_s_pfc_lowercontinuationcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_lowercontinuationcoefficientscoefficientsum_body_steps = fs_r_pfc_lowercontinuationcoefficientscoefficientsum_body_steps + fs_a_pfc_lowercontinuationcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_lowercontinuationcoefficientscoefficientresiduebound. pfa_gap_lowercontinuationcoefficientscoefficientresiduebound + S (pfc_value_lowercontinuationcoefficients) = ((p))) /\ ((exists pfa_offset_left_lowercontinuationcoefficientscoefficientresiduecongruence pfa_offset_right_lowercontinuationcoefficientscoefficientresiduecongruence. (pfc_natural_sum_lowercontinuationcoefficientscoefficient) + ((p)) * pfa_offset_left_lowercontinuationcoefficientscoefficientresiduecongruence = (pfc_value_lowercontinuationcoefficients) + ((p)) * pfa_offset_right_lowercontinuationcoefficientscoefficientresiduecongruence))))))))))))))))))

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