FpConvolutionPrefix(p,ab,ac,L,bb,bc,M,cb,cc,l)

forall pfc_index_lowercontinuation. (exists pfa_gap_lowercontinuationbound. pfa_gap_lowercontinuationbound + S (pfc_index_lowercontinuation) = ((l))) -> exists pfc_value_lowercontinuation. ((((exists ff_h_pfp_lowercontinuationentry. ff_h_pfp_lowercontinuationentry + S (pfc_value_lowercontinuation) = S ((S (pfc_index_lowercontinuation)) * (cc))) /\ exists ff_q_pfp_lowercontinuationentry. (cb) = ff_q_pfp_lowercontinuationentry * S ((S (pfc_index_lowercontinuation)) * (cc)) + (pfc_value_lowercontinuation))) /\ ((exists pfc_terms_code_lowercontinuationcoefficient pfc_terms_scale_lowercontinuationcoefficient pfc_natural_sum_lowercontinuationcoefficient. ((forall pfc_index_lowercontinuationcoefficientdiagonal. (exists pfa_gap_lowercontinuationcoefficientdiagonalbound. pfa_gap_lowercontinuationcoefficientdiagonalbound + S (pfc_index_lowercontinuationcoefficientdiagonal) = (S (pfc_index_lowercontinuation))) -> exists pfc_value_lowercontinuationcoefficientdiagonal. ((((exists ff_h_pfp_lowercontinuationcoefficientdiagonalentry. ff_h_pfp_lowercontinuationcoefficientdiagonalentry + S (pfc_value_lowercontinuationcoefficientdiagonal) = S ((S (pfc_index_lowercontinuationcoefficientdiagonal)) * pfc_terms_scale_lowercontinuationcoefficient)) /\ exists ff_q_pfp_lowercontinuationcoefficientdiagonalentry. pfc_terms_code_lowercontinuationcoefficient = ff_q_pfp_lowercontinuationcoefficientdiagonalentry * S ((S (pfc_index_lowercontinuationcoefficientdiagonal)) * pfc_terms_scale_lowercontinuationcoefficient) + (pfc_value_lowercontinuationcoefficientdiagonal))) /\ ((exists pfc_complement_lowercontinuationcoefficientdiagonalterm pfc_left_lowercontinuationcoefficientdiagonalterm pfc_right_lowercontinuationcoefficientdiagonalterm. (((pfc_index_lowercontinuationcoefficientdiagonal)+pfc_complement_lowercontinuationcoefficientdiagonalterm=(pfc_index_lowercontinuation)) /\ ((((((exists pfa_gap_lowercontinuationcoefficientdiagonaltermleftinside. pfa_gap_lowercontinuationcoefficientdiagonaltermleftinside + S (pfc_index_lowercontinuationcoefficientdiagonal) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationcoefficientdiagonaltermleftentry. ff_h_pfp_lowercontinuationcoefficientdiagonaltermleftentry + S (pfc_left_lowercontinuationcoefficientdiagonalterm) = S ((S (pfc_index_lowercontinuationcoefficientdiagonal)) * (ac))) /\ exists ff_q_pfp_lowercontinuationcoefficientdiagonaltermleftentry. (ab) = ff_q_pfp_lowercontinuationcoefficientdiagonaltermleftentry * S ((S (pfc_index_lowercontinuationcoefficientdiagonal)) * (ac)) + (pfc_left_lowercontinuationcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_lowercontinuationcoefficientdiagonaltermleftoutside. pfc_gap_lowercontinuationcoefficientdiagonaltermleftoutside+((L))=(pfc_index_lowercontinuationcoefficientdiagonal)) /\ (((pfc_left_lowercontinuationcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_lowercontinuationcoefficientdiagonaltermrightinside. pfa_gap_lowercontinuationcoefficientdiagonaltermrightinside + S (pfc_complement_lowercontinuationcoefficientdiagonalterm) = ((M))) /\ ((((exists ff_h_pfp_lowercontinuationcoefficientdiagonaltermrightentry. ff_h_pfp_lowercontinuationcoefficientdiagonaltermrightentry + S (pfc_right_lowercontinuationcoefficientdiagonalterm) = S ((S (pfc_complement_lowercontinuationcoefficientdiagonalterm)) * (bc))) /\ exists ff_q_pfp_lowercontinuationcoefficientdiagonaltermrightentry. (bb) = ff_q_pfp_lowercontinuationcoefficientdiagonaltermrightentry * S ((S (pfc_complement_lowercontinuationcoefficientdiagonalterm)) * (bc)) + (pfc_right_lowercontinuationcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_lowercontinuationcoefficientdiagonaltermrightoutside. pfc_gap_lowercontinuationcoefficientdiagonaltermrightoutside+((M))=(pfc_complement_lowercontinuationcoefficientdiagonalterm)) /\ (((pfc_right_lowercontinuationcoefficientdiagonalterm)=0))))) /\ (((pfc_value_lowercontinuationcoefficientdiagonal)=pfc_left_lowercontinuationcoefficientdiagonalterm*pfc_right_lowercontinuationcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_lowercontinuationcoefficientsum fs_v_pfc_lowercontinuationcoefficientsum. ((((exists fs_h_pfc_lowercontinuationcoefficientsum_body_start. fs_h_pfc_lowercontinuationcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_lowercontinuationcoefficientsum)) /\ exists fs_q_pfc_lowercontinuationcoefficientsum_body_start. fs_u_pfc_lowercontinuationcoefficientsum = fs_q_pfc_lowercontinuationcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_lowercontinuationcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_lowercontinuationcoefficientsum_body_terminal. fs_h_pfc_lowercontinuationcoefficientsum_body_terminal + S (pfc_natural_sum_lowercontinuationcoefficient) = S ((S (S (pfc_index_lowercontinuation))) * fs_v_pfc_lowercontinuationcoefficientsum)) /\ exists fs_q_pfc_lowercontinuationcoefficientsum_body_terminal. fs_u_pfc_lowercontinuationcoefficientsum = fs_q_pfc_lowercontinuationcoefficientsum_body_terminal * S ((S (S (pfc_index_lowercontinuation))) * fs_v_pfc_lowercontinuationcoefficientsum) + (pfc_natural_sum_lowercontinuationcoefficient))) /\ forall fs_i_pfc_lowercontinuationcoefficientsum_body_steps. (exists fs_lt_pfc_lowercontinuationcoefficientsum_body_steps_bound. fs_lt_pfc_lowercontinuationcoefficientsum_body_steps_bound + S fs_i_pfc_lowercontinuationcoefficientsum_body_steps = S (pfc_index_lowercontinuation)) -> exists fs_a_pfc_lowercontinuationcoefficientsum_body_steps fs_r_pfc_lowercontinuationcoefficientsum_body_steps fs_s_pfc_lowercontinuationcoefficientsum_body_steps. ((((exists fs_h_pfc_lowercontinuationcoefficientsum_body_steps_summand. fs_h_pfc_lowercontinuationcoefficientsum_body_steps_summand + S (fs_a_pfc_lowercontinuationcoefficientsum_body_steps) = S ((S (fs_i_pfc_lowercontinuationcoefficientsum_body_steps)) * pfc_terms_scale_lowercontinuationcoefficient)) /\ exists fs_q_pfc_lowercontinuationcoefficientsum_body_steps_summand. pfc_terms_code_lowercontinuationcoefficient = fs_q_pfc_lowercontinuationcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_lowercontinuationcoefficientsum_body_steps)) * pfc_terms_scale_lowercontinuationcoefficient) + (fs_a_pfc_lowercontinuationcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_lowercontinuationcoefficientsum_body_steps_partial. fs_h_pfc_lowercontinuationcoefficientsum_body_steps_partial + S (fs_r_pfc_lowercontinuationcoefficientsum_body_steps) = S ((S (fs_i_pfc_lowercontinuationcoefficientsum_body_steps)) * fs_v_pfc_lowercontinuationcoefficientsum)) /\ exists fs_q_pfc_lowercontinuationcoefficientsum_body_steps_partial. fs_u_pfc_lowercontinuationcoefficientsum = fs_q_pfc_lowercontinuationcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_lowercontinuationcoefficientsum_body_steps)) * fs_v_pfc_lowercontinuationcoefficientsum) + (fs_r_pfc_lowercontinuationcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_lowercontinuationcoefficientsum_body_steps_successor. fs_h_pfc_lowercontinuationcoefficientsum_body_steps_successor + S (fs_s_pfc_lowercontinuationcoefficientsum_body_steps) = S ((S (S fs_i_pfc_lowercontinuationcoefficientsum_body_steps)) * fs_v_pfc_lowercontinuationcoefficientsum)) /\ exists fs_q_pfc_lowercontinuationcoefficientsum_body_steps_successor. fs_u_pfc_lowercontinuationcoefficientsum = fs_q_pfc_lowercontinuationcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_lowercontinuationcoefficientsum_body_steps)) * fs_v_pfc_lowercontinuationcoefficientsum) + (fs_s_pfc_lowercontinuationcoefficientsum_body_steps))) /\ fs_s_pfc_lowercontinuationcoefficientsum_body_steps = fs_r_pfc_lowercontinuationcoefficientsum_body_steps + fs_a_pfc_lowercontinuationcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_lowercontinuationcoefficientresiduebound. pfa_gap_lowercontinuationcoefficientresiduebound + S (pfc_value_lowercontinuation) = ((p))) /\ ((exists pfa_offset_left_lowercontinuationcoefficientresiduecongruence pfa_offset_right_lowercontinuationcoefficientresiduecongruence. (pfc_natural_sum_lowercontinuationcoefficient) + ((p)) * pfa_offset_left_lowercontinuationcoefficientresiduecongruence = (pfc_value_lowercontinuation) + ((p)) * pfa_offset_right_lowercontinuationcoefficientresiduecongruence)))))))))))

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