prime_field_polynomial_quotient_prefix_convolution_entry

forall p k ab ac bb bc d qb qc N b i r. (~((p) = 1) /\ forall pfa_factor_left_division_match_prime pfa_factor_right_division_match_prime. (p) = pfa_factor_left_division_match_prime * pfa_factor_right_division_match_prime -> pfa_factor_left_division_match_prime = 1 \/ pfa_factor_right_division_match_prime = 1) -> (((exists ff_h_pfp_division_match_head. ff_h_pfp_division_match_head + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_match_head. bb = ff_q_pfp_division_match_head * S ((S (0)) * bc) + (b))) -> (((~((b) = 0)) /\ ((((exists pfa_gap_division_match_inversemultiplicationleft. pfa_gap_division_match_inversemultiplicationleft + S (b) = (p)) /\ (((exists pfa_gap_division_match_inversemultiplicationright. pfa_gap_division_match_inversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_division_match_inversemultiplicationresultbound. pfa_gap_division_match_inversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_match_inversemultiplicationresultcongruence pfa_offset_right_division_match_inversemultiplicationresultcongruence. ((b) * (k)) + (p) * pfa_offset_left_division_match_inversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_match_inversemultiplicationresultcongruence)))))))))))) -> (forall pfd_index_division_match_execution. (exists pfa_gap_division_match_executionbound. pfa_gap_division_match_executionbound + S (pfd_index_division_match_execution) = (N)) -> exists pfd_value_division_match_execution. ((((exists ff_h_pfp_division_match_executionentry. ff_h_pfp_division_match_executionentry + S (pfd_value_division_match_execution) = S ((S (pfd_index_division_match_execution)) * qc)) /\ exists ff_q_pfp_division_match_executionentry. qb = ff_q_pfp_division_match_executionentry * S ((S (pfd_index_division_match_execution)) * qc) + (pfd_value_division_match_execution))) /\ ((exists pfd_input_division_match_executionstep pfd_previous_division_match_executionstep pfd_difference_division_match_executionstep. ((((exists ff_h_pfp_division_match_executionstepinput. ff_h_pfp_division_match_executionstepinput + S (pfd_input_division_match_executionstep) = S ((S (pfd_index_division_match_execution)) * ac)) /\ exists ff_q_pfp_division_match_executionstepinput. ab = ff_q_pfp_division_match_executionstepinput * S ((S (pfd_index_division_match_execution)) * ac) + (pfd_input_division_match_executionstep))) /\ (((exists pfc_terms_code_division_match_executionstepprevious pfc_terms_scale_division_match_executionstepprevious pfc_natural_sum_division_match_executionstepprevious. ((forall pfc_index_division_match_executionsteppreviousdiagonal. (exists pfa_gap_division_match_executionsteppreviousdiagonalbound. pfa_gap_division_match_executionsteppreviousdiagonalbound + S (pfc_index_division_match_executionsteppreviousdiagonal) = (S (pfd_index_division_match_execution))) -> exists pfc_value_division_match_executionsteppreviousdiagonal. ((((exists ff_h_pfp_division_match_executionsteppreviousdiagonalentry. ff_h_pfp_division_match_executionsteppreviousdiagonalentry + S (pfc_value_division_match_executionsteppreviousdiagonal) = S ((S (pfc_index_division_match_executionsteppreviousdiagonal)) * pfc_terms_scale_division_match_executionstepprevious)) /\ exists ff_q_pfp_division_match_executionsteppreviousdiagonalentry. pfc_terms_code_division_match_executionstepprevious = ff_q_pfp_division_match_executionsteppreviousdiagonalentry * S ((S (pfc_index_division_match_executionsteppreviousdiagonal)) * pfc_terms_scale_division_match_executionstepprevious) + (pfc_value_division_match_executionsteppreviousdiagonal))) /\ ((exists pfc_complement_division_match_executionsteppreviousdiagonalterm pfc_left_division_match_executionsteppreviousdiagonalterm pfc_right_division_match_executionsteppreviousdiagonalterm. (((pfc_index_division_match_executionsteppreviousdiagonal)+pfc_complement_division_match_executionsteppreviousdiagonalterm=(pfd_index_division_match_execution)) /\ ((((((exists pfa_gap_division_match_executionsteppreviousdiagonaltermleftinside. pfa_gap_division_match_executionsteppreviousdiagonaltermleftinside + S (pfc_index_division_match_executionsteppreviousdiagonal) = (pfd_index_division_match_execution)) /\ ((((exists ff_h_pfp_division_match_executionsteppreviousdiagonaltermleftentry. ff_h_pfp_division_match_executionsteppreviousdiagonaltermleftentry + S (pfc_left_division_match_executionsteppreviousdiagonalterm) = S ((S (pfc_index_division_match_executionsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_match_executionsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_match_executionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_match_executionsteppreviousdiagonal)) * qc) + (pfc_left_division_match_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_match_executionsteppreviousdiagonaltermleftoutside. pfc_gap_division_match_executionsteppreviousdiagonaltermleftoutside+(pfd_index_division_match_execution)=(pfc_index_division_match_executionsteppreviousdiagonal)) /\ (((pfc_left_division_match_executionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_match_executionsteppreviousdiagonaltermrightinside. pfa_gap_division_match_executionsteppreviousdiagonaltermrightinside + S (pfc_complement_division_match_executionsteppreviousdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_match_executionsteppreviousdiagonaltermrightentry. ff_h_pfp_division_match_executionsteppreviousdiagonaltermrightentry + S (pfc_right_division_match_executionsteppreviousdiagonalterm) = S ((S (pfc_complement_division_match_executionsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_match_executionsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_match_executionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_match_executionsteppreviousdiagonalterm)) * bc) + (pfc_right_division_match_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_match_executionsteppreviousdiagonaltermrightoutside. pfc_gap_division_match_executionsteppreviousdiagonaltermrightoutside+(S d)=(pfc_complement_division_match_executionsteppreviousdiagonalterm)) /\ (((pfc_right_division_match_executionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_match_executionsteppreviousdiagonal)=pfc_left_division_match_executionsteppreviousdiagonalterm*pfc_right_division_match_executionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_match_executionstepprevioussum fs_v_pfc_division_match_executionstepprevioussum. ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_start. fs_h_pfc_division_match_executionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_match_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_start. fs_u_pfc_division_match_executionstepprevioussum = fs_q_pfc_division_match_executionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_match_executionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_terminal. fs_h_pfc_division_match_executionstepprevioussum_body_terminal + S (pfc_natural_sum_division_match_executionstepprevious) = S ((S (S (pfd_index_division_match_execution))) * fs_v_pfc_division_match_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_terminal. fs_u_pfc_division_match_executionstepprevioussum = fs_q_pfc_division_match_executionstepprevioussum_body_terminal * S ((S (S (pfd_index_division_match_execution))) * fs_v_pfc_division_match_executionstepprevioussum) + (pfc_natural_sum_division_match_executionstepprevious))) /\ forall fs_i_pfc_division_match_executionstepprevioussum_body_steps. (exists fs_lt_pfc_division_match_executionstepprevioussum_body_steps_bound. fs_lt_pfc_division_match_executionstepprevioussum_body_steps_bound + S fs_i_pfc_division_match_executionstepprevioussum_body_steps = S (pfd_index_division_match_execution)) -> exists fs_a_pfc_division_match_executionstepprevioussum_body_steps fs_r_pfc_division_match_executionstepprevioussum_body_steps fs_s_pfc_division_match_executionstepprevioussum_body_steps. ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_steps_summand. fs_h_pfc_division_match_executionstepprevioussum_body_steps_summand + S (fs_a_pfc_division_match_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_match_executionstepprevious)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_steps_summand. pfc_terms_code_division_match_executionstepprevious = fs_q_pfc_division_match_executionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_match_executionstepprevious) + (fs_a_pfc_division_match_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_steps_partial. fs_h_pfc_division_match_executionstepprevioussum_body_steps_partial + S (fs_r_pfc_division_match_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_steps_partial. fs_u_pfc_division_match_executionstepprevioussum = fs_q_pfc_division_match_executionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_executionstepprevioussum) + (fs_r_pfc_division_match_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_steps_successor. fs_h_pfc_division_match_executionstepprevioussum_body_steps_successor + S (fs_s_pfc_division_match_executionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_steps_successor. fs_u_pfc_division_match_executionstepprevioussum = fs_q_pfc_division_match_executionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_executionstepprevioussum) + (fs_s_pfc_division_match_executionstepprevioussum_body_steps))) /\ fs_s_pfc_division_match_executionstepprevioussum_body_steps = fs_r_pfc_division_match_executionstepprevioussum_body_steps + fs_a_pfc_division_match_executionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_match_executionsteppreviousresiduebound. pfa_gap_division_match_executionsteppreviousresiduebound + S (pfd_previous_division_match_executionstep) = (p)) /\ ((exists pfa_offset_left_division_match_executionsteppreviousresiduecongruence pfa_offset_right_division_match_executionsteppreviousresiduecongruence. (pfc_natural_sum_division_match_executionstepprevious) + (p) * pfa_offset_left_division_match_executionsteppreviousresiduecongruence = (pfd_previous_division_match_executionstep) + (p) * pfa_offset_right_division_match_executionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_match_executionstepsubtractleft. pfa_gap_division_match_executionstepsubtractleft + S (pfd_previous_division_match_executionstep) = (p)) /\ (((exists pfa_gap_division_match_executionstepsubtractright. pfa_gap_division_match_executionstepsubtractright + S (pfd_difference_division_match_executionstep) = (p)) /\ ((((exists pfa_gap_division_match_executionstepsubtractresultbound. pfa_gap_division_match_executionstepsubtractresultbound + S (pfd_input_division_match_executionstep) = (p)) /\ ((exists pfa_offset_left_division_match_executionstepsubtractresultcongruence pfa_offset_right_division_match_executionstepsubtractresultcongruence. ((pfd_previous_division_match_executionstep) + (pfd_difference_division_match_executionstep)) + (p) * pfa_offset_left_division_match_executionstepsubtractresultcongruence = (pfd_input_division_match_executionstep) + (p) * pfa_offset_right_division_match_executionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_match_executionstepmultiplyleft. pfa_gap_division_match_executionstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_match_executionstepmultiplyright. pfa_gap_division_match_executionstepmultiplyright + S (pfd_difference_division_match_executionstep) = (p)) /\ ((((exists pfa_gap_division_match_executionstepmultiplyresultbound. pfa_gap_division_match_executionstepmultiplyresultbound + S (pfd_value_division_match_execution) = (p)) /\ ((exists pfa_offset_left_division_match_executionstepmultiplyresultcongruence pfa_offset_right_division_match_executionstepmultiplyresultcongruence. ((k) * (pfd_difference_division_match_executionstep)) + (p) * pfa_offset_left_division_match_executionstepmultiplyresultcongruence = (pfd_value_division_match_execution) + (p) * pfa_offset_right_division_match_executionstepmultiplyresultcongruence))))))))))))))))))) -> (exists pfa_gap_division_match_index. pfa_gap_division_match_index + S (i) = (N)) -> (exists pfc_terms_code_division_match_actual_coefficient pfc_terms_scale_division_match_actual_coefficient pfc_natural_sum_division_match_actual_coefficient. ((forall pfc_index_division_match_actual_coefficientdiagonal. (exists pfa_gap_division_match_actual_coefficientdiagonalbound. pfa_gap_division_match_actual_coefficientdiagonalbound + S (pfc_index_division_match_actual_coefficientdiagonal) = (S (i))) -> exists pfc_value_division_match_actual_coefficientdiagonal. ((((exists ff_h_pfp_division_match_actual_coefficientdiagonalentry. ff_h_pfp_division_match_actual_coefficientdiagonalentry + S (pfc_value_division_match_actual_coefficientdiagonal) = S ((S (pfc_index_division_match_actual_coefficientdiagonal)) * pfc_terms_scale_division_match_actual_coefficient)) /\ exists ff_q_pfp_division_match_actual_coefficientdiagonalentry. pfc_terms_code_division_match_actual_coefficient = ff_q_pfp_division_match_actual_coefficientdiagonalentry * S ((S (pfc_index_division_match_actual_coefficientdiagonal)) * pfc_terms_scale_division_match_actual_coefficient) + (pfc_value_division_match_actual_coefficientdiagonal))) /\ ((exists pfc_complement_division_match_actual_coefficientdiagonalterm pfc_left_division_match_actual_coefficientdiagonalterm pfc_right_division_match_actual_coefficientdiagonalterm. (((pfc_index_division_match_actual_coefficientdiagonal)+pfc_complement_division_match_actual_coefficientdiagonalterm=(i)) /\ ((((((exists pfa_gap_division_match_actual_coefficientdiagonaltermleftinside. pfa_gap_division_match_actual_coefficientdiagonaltermleftinside + S (pfc_index_division_match_actual_coefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_division_match_actual_coefficientdiagonaltermleftentry. ff_h_pfp_division_match_actual_coefficientdiagonaltermleftentry + S (pfc_left_division_match_actual_coefficientdiagonalterm) = S ((S (pfc_index_division_match_actual_coefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_match_actual_coefficientdiagonaltermleftentry. qb = ff_q_pfp_division_match_actual_coefficientdiagonaltermleftentry * S ((S (pfc_index_division_match_actual_coefficientdiagonal)) * qc) + (pfc_left_division_match_actual_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_match_actual_coefficientdiagonaltermleftoutside. pfc_gap_division_match_actual_coefficientdiagonaltermleftoutside+(N)=(pfc_index_division_match_actual_coefficientdiagonal)) /\ (((pfc_left_division_match_actual_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_match_actual_coefficientdiagonaltermrightinside. pfa_gap_division_match_actual_coefficientdiagonaltermrightinside + S (pfc_complement_division_match_actual_coefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_match_actual_coefficientdiagonaltermrightentry. ff_h_pfp_division_match_actual_coefficientdiagonaltermrightentry + S (pfc_right_division_match_actual_coefficientdiagonalterm) = S ((S (pfc_complement_division_match_actual_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_match_actual_coefficientdiagonaltermrightentry. bb = ff_q_pfp_division_match_actual_coefficientdiagonaltermrightentry * S ((S (pfc_complement_division_match_actual_coefficientdiagonalterm)) * bc) + (pfc_right_division_match_actual_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_match_actual_coefficientdiagonaltermrightoutside. pfc_gap_division_match_actual_coefficientdiagonaltermrightoutside+(S d)=(pfc_complement_division_match_actual_coefficientdiagonalterm)) /\ (((pfc_right_division_match_actual_coefficientdiagonalterm)=0))))) /\ (((pfc_value_division_match_actual_coefficientdiagonal)=pfc_left_division_match_actual_coefficientdiagonalterm*pfc_right_division_match_actual_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_match_actual_coefficientsum fs_v_pfc_division_match_actual_coefficientsum. ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_start. fs_h_pfc_division_match_actual_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_match_actual_coefficientsum)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_start. fs_u_pfc_division_match_actual_coefficientsum = fs_q_pfc_division_match_actual_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_match_actual_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_terminal. fs_h_pfc_division_match_actual_coefficientsum_body_terminal + S (pfc_natural_sum_division_match_actual_coefficient) = S ((S (S (i))) * fs_v_pfc_division_match_actual_coefficientsum)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_terminal. fs_u_pfc_division_match_actual_coefficientsum = fs_q_pfc_division_match_actual_coefficientsum_body_terminal * S ((S (S (i))) * fs_v_pfc_division_match_actual_coefficientsum) + (pfc_natural_sum_division_match_actual_coefficient))) /\ forall fs_i_pfc_division_match_actual_coefficientsum_body_steps. (exists fs_lt_pfc_division_match_actual_coefficientsum_body_steps_bound. fs_lt_pfc_division_match_actual_coefficientsum_body_steps_bound + S fs_i_pfc_division_match_actual_coefficientsum_body_steps = S (i)) -> exists fs_a_pfc_division_match_actual_coefficientsum_body_steps fs_r_pfc_division_match_actual_coefficientsum_body_steps fs_s_pfc_division_match_actual_coefficientsum_body_steps. ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_steps_summand. fs_h_pfc_division_match_actual_coefficientsum_body_steps_summand + S (fs_a_pfc_division_match_actual_coefficientsum_body_steps) = S ((S (fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * pfc_terms_scale_division_match_actual_coefficient)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_steps_summand. pfc_terms_code_division_match_actual_coefficient = fs_q_pfc_division_match_actual_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * pfc_terms_scale_division_match_actual_coefficient) + (fs_a_pfc_division_match_actual_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_steps_partial. fs_h_pfc_division_match_actual_coefficientsum_body_steps_partial + S (fs_r_pfc_division_match_actual_coefficientsum_body_steps) = S ((S (fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * fs_v_pfc_division_match_actual_coefficientsum)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_steps_partial. fs_u_pfc_division_match_actual_coefficientsum = fs_q_pfc_division_match_actual_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * fs_v_pfc_division_match_actual_coefficientsum) + (fs_r_pfc_division_match_actual_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_steps_successor. fs_h_pfc_division_match_actual_coefficientsum_body_steps_successor + S (fs_s_pfc_division_match_actual_coefficientsum_body_steps) = S ((S (S fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * fs_v_pfc_division_match_actual_coefficientsum)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_steps_successor. fs_u_pfc_division_match_actual_coefficientsum = fs_q_pfc_division_match_actual_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * fs_v_pfc_division_match_actual_coefficientsum) + (fs_s_pfc_division_match_actual_coefficientsum_body_steps))) /\ fs_s_pfc_division_match_actual_coefficientsum_body_steps = fs_r_pfc_division_match_actual_coefficientsum_body_steps + fs_a_pfc_division_match_actual_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_match_actual_coefficientresiduebound. pfa_gap_division_match_actual_coefficientresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_division_match_actual_coefficientresiduecongruence pfa_offset_right_division_match_actual_coefficientresiduecongruence. (pfc_natural_sum_division_match_actual_coefficient) + (p) * pfa_offset_left_division_match_actual_coefficientresiduecongruence = (r) + (p) * pfa_offset_right_division_match_actual_coefficientresiduecongruence))))))))) -> (((exists ff_h_pfp_division_match_input. ff_h_pfp_division_match_input + S (r) = S ((S (i)) * ac)) /\ exists ff_q_pfp_division_match_input. ab = ff_q_pfp_division_match_input * S ((S (i)) * ac) + (r)))