FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r)

exists pfc_terms_code_lowercontinuation pfc_terms_scale_lowercontinuation pfc_natural_sum_lowercontinuation. ((forall pfc_index_lowercontinuationdiagonal. (exists pfa_gap_lowercontinuationdiagonalbound. pfa_gap_lowercontinuationdiagonalbound + S (pfc_index_lowercontinuationdiagonal) = (S ((i)))) -> exists pfc_value_lowercontinuationdiagonal. ((((exists ff_h_pfp_lowercontinuationdiagonalentry. ff_h_pfp_lowercontinuationdiagonalentry + S (pfc_value_lowercontinuationdiagonal) = S ((S (pfc_index_lowercontinuationdiagonal)) * pfc_terms_scale_lowercontinuation)) /\ exists ff_q_pfp_lowercontinuationdiagonalentry. pfc_terms_code_lowercontinuation = ff_q_pfp_lowercontinuationdiagonalentry * S ((S (pfc_index_lowercontinuationdiagonal)) * pfc_terms_scale_lowercontinuation) + (pfc_value_lowercontinuationdiagonal))) /\ ((exists pfc_complement_lowercontinuationdiagonalterm pfc_left_lowercontinuationdiagonalterm pfc_right_lowercontinuationdiagonalterm. (((pfc_index_lowercontinuationdiagonal)+pfc_complement_lowercontinuationdiagonalterm=((i))) /\ ((((((exists pfa_gap_lowercontinuationdiagonaltermleftinside. pfa_gap_lowercontinuationdiagonaltermleftinside + S (pfc_index_lowercontinuationdiagonal) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationdiagonaltermleftentry. ff_h_pfp_lowercontinuationdiagonaltermleftentry + S (pfc_left_lowercontinuationdiagonalterm) = S ((S (pfc_index_lowercontinuationdiagonal)) * (ac))) /\ exists ff_q_pfp_lowercontinuationdiagonaltermleftentry. (ab) = ff_q_pfp_lowercontinuationdiagonaltermleftentry * S ((S (pfc_index_lowercontinuationdiagonal)) * (ac)) + (pfc_left_lowercontinuationdiagonalterm)))))) \/ (((exists pfc_gap_lowercontinuationdiagonaltermleftoutside. pfc_gap_lowercontinuationdiagonaltermleftoutside+((L))=(pfc_index_lowercontinuationdiagonal)) /\ (((pfc_left_lowercontinuationdiagonalterm)=0))))) /\ ((((((exists pfa_gap_lowercontinuationdiagonaltermrightinside. pfa_gap_lowercontinuationdiagonaltermrightinside + S (pfc_complement_lowercontinuationdiagonalterm) = ((M))) /\ ((((exists ff_h_pfp_lowercontinuationdiagonaltermrightentry. ff_h_pfp_lowercontinuationdiagonaltermrightentry + S (pfc_right_lowercontinuationdiagonalterm) = S ((S (pfc_complement_lowercontinuationdiagonalterm)) * (bc))) /\ exists ff_q_pfp_lowercontinuationdiagonaltermrightentry. (bb) = ff_q_pfp_lowercontinuationdiagonaltermrightentry * S ((S (pfc_complement_lowercontinuationdiagonalterm)) * (bc)) + (pfc_right_lowercontinuationdiagonalterm)))))) \/ (((exists pfc_gap_lowercontinuationdiagonaltermrightoutside. pfc_gap_lowercontinuationdiagonaltermrightoutside+((M))=(pfc_complement_lowercontinuationdiagonalterm)) /\ (((pfc_right_lowercontinuationdiagonalterm)=0))))) /\ (((pfc_value_lowercontinuationdiagonal)=pfc_left_lowercontinuationdiagonalterm*pfc_right_lowercontinuationdiagonalterm))))))))))) /\ (((exists fs_u_pfc_lowercontinuationsum fs_v_pfc_lowercontinuationsum. ((((exists fs_h_pfc_lowercontinuationsum_body_start. fs_h_pfc_lowercontinuationsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_lowercontinuationsum)) /\ exists fs_q_pfc_lowercontinuationsum_body_start. fs_u_pfc_lowercontinuationsum = fs_q_pfc_lowercontinuationsum_body_start * S ((S (0)) * fs_v_pfc_lowercontinuationsum) + (0))) /\ ((((exists fs_h_pfc_lowercontinuationsum_body_terminal. fs_h_pfc_lowercontinuationsum_body_terminal + S (pfc_natural_sum_lowercontinuation) = S ((S (S ((i)))) * fs_v_pfc_lowercontinuationsum)) /\ exists fs_q_pfc_lowercontinuationsum_body_terminal. fs_u_pfc_lowercontinuationsum = fs_q_pfc_lowercontinuationsum_body_terminal * S ((S (S ((i)))) * fs_v_pfc_lowercontinuationsum) + (pfc_natural_sum_lowercontinuation))) /\ forall fs_i_pfc_lowercontinuationsum_body_steps. (exists fs_lt_pfc_lowercontinuationsum_body_steps_bound. fs_lt_pfc_lowercontinuationsum_body_steps_bound + S fs_i_pfc_lowercontinuationsum_body_steps = S ((i))) -> exists fs_a_pfc_lowercontinuationsum_body_steps fs_r_pfc_lowercontinuationsum_body_steps fs_s_pfc_lowercontinuationsum_body_steps. ((((exists fs_h_pfc_lowercontinuationsum_body_steps_summand. fs_h_pfc_lowercontinuationsum_body_steps_summand + S (fs_a_pfc_lowercontinuationsum_body_steps) = S ((S (fs_i_pfc_lowercontinuationsum_body_steps)) * pfc_terms_scale_lowercontinuation)) /\ exists fs_q_pfc_lowercontinuationsum_body_steps_summand. pfc_terms_code_lowercontinuation = fs_q_pfc_lowercontinuationsum_body_steps_summand * S ((S (fs_i_pfc_lowercontinuationsum_body_steps)) * pfc_terms_scale_lowercontinuation) + (fs_a_pfc_lowercontinuationsum_body_steps))) /\ ((((exists fs_h_pfc_lowercontinuationsum_body_steps_partial. fs_h_pfc_lowercontinuationsum_body_steps_partial + S (fs_r_pfc_lowercontinuationsum_body_steps) = S ((S (fs_i_pfc_lowercontinuationsum_body_steps)) * fs_v_pfc_lowercontinuationsum)) /\ exists fs_q_pfc_lowercontinuationsum_body_steps_partial. fs_u_pfc_lowercontinuationsum = fs_q_pfc_lowercontinuationsum_body_steps_partial * S ((S (fs_i_pfc_lowercontinuationsum_body_steps)) * fs_v_pfc_lowercontinuationsum) + (fs_r_pfc_lowercontinuationsum_body_steps))) /\ ((((exists fs_h_pfc_lowercontinuationsum_body_steps_successor. fs_h_pfc_lowercontinuationsum_body_steps_successor + S (fs_s_pfc_lowercontinuationsum_body_steps) = S ((S (S fs_i_pfc_lowercontinuationsum_body_steps)) * fs_v_pfc_lowercontinuationsum)) /\ exists fs_q_pfc_lowercontinuationsum_body_steps_successor. fs_u_pfc_lowercontinuationsum = fs_q_pfc_lowercontinuationsum_body_steps_successor * S ((S (S fs_i_pfc_lowercontinuationsum_body_steps)) * fs_v_pfc_lowercontinuationsum) + (fs_s_pfc_lowercontinuationsum_body_steps))) /\ fs_s_pfc_lowercontinuationsum_body_steps = fs_r_pfc_lowercontinuationsum_body_steps + fs_a_pfc_lowercontinuationsum_body_steps)))))) /\ ((((exists pfa_gap_lowercontinuationresiduebound. pfa_gap_lowercontinuationresiduebound + S ((r)) = ((p))) /\ ((exists pfa_offset_left_lowercontinuationresiduecongruence pfa_offset_right_lowercontinuationresiduecongruence. (pfc_natural_sum_lowercontinuation) + ((p)) * pfa_offset_left_lowercontinuationresiduecongruence = ((r)) + ((p)) * pfa_offset_right_lowercontinuationresiduecongruence))))))))

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