prime_field_convolution_coefficient_right_scale

Exact expanded first-order arithmetic statement

forall p k ab ac L bb bc M sb sc i c r. (((exists pfa_gap_scalar_coefficient_operationscalar. pfa_gap_scalar_coefficient_operationscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_coefficient_operation. (exists pfa_gap_scalar_coefficient_operationindex. pfa_gap_scalar_coefficient_operationindex + S (pfp_index_scalar_coefficient_operation) = (M)) -> exists pfp_source_scalar_coefficient_operation pfp_value_scalar_coefficient_operation. ((((exists ff_h_pfp_scalar_coefficient_operationsource. ff_h_pfp_scalar_coefficient_operationsource + S (pfp_source_scalar_coefficient_operation) = S ((S (pfp_index_scalar_coefficient_operation)) * bc)) /\ exists ff_q_pfp_scalar_coefficient_operationsource. bb = ff_q_pfp_scalar_coefficient_operationsource * S ((S (pfp_index_scalar_coefficient_operation)) * bc) + (pfp_source_scalar_coefficient_operation))) /\ (((((exists ff_h_pfp_scalar_coefficient_operationtarget. ff_h_pfp_scalar_coefficient_operationtarget + S (pfp_value_scalar_coefficient_operation) = S ((S (pfp_index_scalar_coefficient_operation)) * sc)) /\ exists ff_q_pfp_scalar_coefficient_operationtarget. sb = ff_q_pfp_scalar_coefficient_operationtarget * S ((S (pfp_index_scalar_coefficient_operation)) * sc) + (pfp_value_scalar_coefficient_operation))) /\ ((((exists pfa_gap_scalar_coefficient_operationoperationleft. pfa_gap_scalar_coefficient_operationoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_coefficient_operationoperationright. pfa_gap_scalar_coefficient_operationoperationright + S (pfp_source_scalar_coefficient_operation) = (p)) /\ ((((exists pfa_gap_scalar_coefficient_operationoperationresultbound. pfa_gap_scalar_coefficient_operationoperationresultbound + S (pfp_value_scalar_coefficient_operation) = (p)) /\ ((exists pfa_offset_left_scalar_coefficient_operationoperationresultcongruence pfa_offset_right_scalar_coefficient_operationoperationresultcongruence. ((k) * (pfp_source_scalar_coefficient_operation)) + (p) * pfa_offset_left_scalar_coefficient_operationoperationresultcongruence = (pfp_value_scalar_coefficient_operation) + (p) * pfa_offset_right_scalar_coefficient_operationoperationresultcongruence))))))))))))))))) -> (exists pfc_terms_code_scalar_coefficient_original pfc_terms_scale_scalar_coefficient_original pfc_natural_sum_scalar_coefficient_original. ((forall pfc_index_scalar_coefficient_originaldiagonal. (exists pfa_gap_scalar_coefficient_originaldiagonalbound. pfa_gap_scalar_coefficient_originaldiagonalbound + S (pfc_index_scalar_coefficient_originaldiagonal) = (S (i))) -> exists pfc_value_scalar_coefficient_originaldiagonal. ((((exists ff_h_pfp_scalar_coefficient_originaldiagonalentry. ff_h_pfp_scalar_coefficient_originaldiagonalentry + S (pfc_value_scalar_coefficient_originaldiagonal) = S ((S (pfc_index_scalar_coefficient_originaldiagonal)) * pfc_terms_scale_scalar_coefficient_original)) /\ exists ff_q_pfp_scalar_coefficient_originaldiagonalentry. pfc_terms_code_scalar_coefficient_original = ff_q_pfp_scalar_coefficient_originaldiagonalentry * S ((S (pfc_index_scalar_coefficient_originaldiagonal)) * pfc_terms_scale_scalar_coefficient_original) + (pfc_value_scalar_coefficient_originaldiagonal))) /\ ((exists pfc_complement_scalar_coefficient_originaldiagonalterm pfc_left_scalar_coefficient_originaldiagonalterm pfc_right_scalar_coefficient_originaldiagonalterm. (((pfc_index_scalar_coefficient_originaldiagonal)+pfc_complement_scalar_coefficient_originaldiagonalterm=(i)) /\ ((((((exists pfa_gap_scalar_coefficient_originaldiagonaltermleftinside. pfa_gap_scalar_coefficient_originaldiagonaltermleftinside + S (pfc_index_scalar_coefficient_originaldiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_coefficient_originaldiagonaltermleftentry. ff_h_pfp_scalar_coefficient_originaldiagonaltermleftentry + S (pfc_left_scalar_coefficient_originaldiagonalterm) = S ((S (pfc_index_scalar_coefficient_originaldiagonal)) * ac)) /\ exists ff_q_pfp_scalar_coefficient_originaldiagonaltermleftentry. ab = ff_q_pfp_scalar_coefficient_originaldiagonaltermleftentry * S ((S (pfc_index_scalar_coefficient_originaldiagonal)) * ac) + (pfc_left_scalar_coefficient_originaldiagonalterm)))))) \/ (((exists pfc_gap_scalar_coefficient_originaldiagonaltermleftoutside. pfc_gap_scalar_coefficient_originaldiagonaltermleftoutside+(L)=(pfc_index_scalar_coefficient_originaldiagonal)) /\ (((pfc_left_scalar_coefficient_originaldiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_coefficient_originaldiagonaltermrightinside. pfa_gap_scalar_coefficient_originaldiagonaltermrightinside + S (pfc_complement_scalar_coefficient_originaldiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_coefficient_originaldiagonaltermrightentry. ff_h_pfp_scalar_coefficient_originaldiagonaltermrightentry + S (pfc_right_scalar_coefficient_originaldiagonalterm) = S ((S (pfc_complement_scalar_coefficient_originaldiagonalterm)) * bc)) /\ exists ff_q_pfp_scalar_coefficient_originaldiagonaltermrightentry. bb = ff_q_pfp_scalar_coefficient_originaldiagonaltermrightentry * S ((S (pfc_complement_scalar_coefficient_originaldiagonalterm)) * bc) + (pfc_right_scalar_coefficient_originaldiagonalterm)))))) \/ (((exists pfc_gap_scalar_coefficient_originaldiagonaltermrightoutside. pfc_gap_scalar_coefficient_originaldiagonaltermrightoutside+(M)=(pfc_complement_scalar_coefficient_originaldiagonalterm)) /\ (((pfc_right_scalar_coefficient_originaldiagonalterm)=0))))) /\ (((pfc_value_scalar_coefficient_originaldiagonal)=pfc_left_scalar_coefficient_originaldiagonalterm*pfc_right_scalar_coefficient_originaldiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_coefficient_originalsum fs_v_pfc_scalar_coefficient_originalsum. ((((exists fs_h_pfc_scalar_coefficient_originalsum_body_start. fs_h_pfc_scalar_coefficient_originalsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_coefficient_originalsum)) /\ exists fs_q_pfc_scalar_coefficient_originalsum_body_start. fs_u_pfc_scalar_coefficient_originalsum = fs_q_pfc_scalar_coefficient_originalsum_body_start * S ((S (0)) * fs_v_pfc_scalar_coefficient_originalsum) + (0))) /\ ((((exists fs_h_pfc_scalar_coefficient_originalsum_body_terminal. fs_h_pfc_scalar_coefficient_originalsum_body_terminal + S (pfc_natural_sum_scalar_coefficient_original) = S ((S (S (i))) * fs_v_pfc_scalar_coefficient_originalsum)) /\ exists fs_q_pfc_scalar_coefficient_originalsum_body_terminal. fs_u_pfc_scalar_coefficient_originalsum = fs_q_pfc_scalar_coefficient_originalsum_body_terminal * S ((S (S (i))) * fs_v_pfc_scalar_coefficient_originalsum) + (pfc_natural_sum_scalar_coefficient_original))) /\ forall fs_i_pfc_scalar_coefficient_originalsum_body_steps. (exists fs_lt_pfc_scalar_coefficient_originalsum_body_steps_bound. fs_lt_pfc_scalar_coefficient_originalsum_body_steps_bound + S fs_i_pfc_scalar_coefficient_originalsum_body_steps = S (i)) -> exists fs_a_pfc_scalar_coefficient_originalsum_body_steps fs_r_pfc_scalar_coefficient_originalsum_body_steps fs_s_pfc_scalar_coefficient_originalsum_body_steps. ((((exists fs_h_pfc_scalar_coefficient_originalsum_body_steps_summand. fs_h_pfc_scalar_coefficient_originalsum_body_steps_summand + S (fs_a_pfc_scalar_coefficient_originalsum_body_steps) = S ((S (fs_i_pfc_scalar_coefficient_originalsum_body_steps)) * pfc_terms_scale_scalar_coefficient_original)) /\ exists fs_q_pfc_scalar_coefficient_originalsum_body_steps_summand. pfc_terms_code_scalar_coefficient_original = fs_q_pfc_scalar_coefficient_originalsum_body_steps_summand * S ((S (fs_i_pfc_scalar_coefficient_originalsum_body_steps)) * pfc_terms_scale_scalar_coefficient_original) + (fs_a_pfc_scalar_coefficient_originalsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_coefficient_originalsum_body_steps_partial. fs_h_pfc_scalar_coefficient_originalsum_body_steps_partial + S (fs_r_pfc_scalar_coefficient_originalsum_body_steps) = S ((S (fs_i_pfc_scalar_coefficient_originalsum_body_steps)) * fs_v_pfc_scalar_coefficient_originalsum)) /\ exists fs_q_pfc_scalar_coefficient_originalsum_body_steps_partial. fs_u_pfc_scalar_coefficient_originalsum = fs_q_pfc_scalar_coefficient_originalsum_body_steps_partial * S ((S (fs_i_pfc_scalar_coefficient_originalsum_body_steps)) * fs_v_pfc_scalar_coefficient_originalsum) + (fs_r_pfc_scalar_coefficient_originalsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_coefficient_originalsum_body_steps_successor. fs_h_pfc_scalar_coefficient_originalsum_body_steps_successor + S (fs_s_pfc_scalar_coefficient_originalsum_body_steps) = S ((S (S fs_i_pfc_scalar_coefficient_originalsum_body_steps)) * fs_v_pfc_scalar_coefficient_originalsum)) /\ exists fs_q_pfc_scalar_coefficient_originalsum_body_steps_successor. fs_u_pfc_scalar_coefficient_originalsum = fs_q_pfc_scalar_coefficient_originalsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_coefficient_originalsum_body_steps)) * fs_v_pfc_scalar_coefficient_originalsum) + (fs_s_pfc_scalar_coefficient_originalsum_body_steps))) /\ fs_s_pfc_scalar_coefficient_originalsum_body_steps = fs_r_pfc_scalar_coefficient_originalsum_body_steps + fs_a_pfc_scalar_coefficient_originalsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_coefficient_originalresiduebound. pfa_gap_scalar_coefficient_originalresiduebound + S (c) = (p)) /\ ((exists pfa_offset_left_scalar_coefficient_originalresiduecongruence pfa_offset_right_scalar_coefficient_originalresiduecongruence. (pfc_natural_sum_scalar_coefficient_original) + (p) * pfa_offset_left_scalar_coefficient_originalresiduecongruence = (c) + (p) * pfa_offset_right_scalar_coefficient_originalresiduecongruence))))))))) -> (exists pfc_terms_code_scalar_coefficient_scaled pfc_terms_scale_scalar_coefficient_scaled pfc_natural_sum_scalar_coefficient_scaled. ((forall pfc_index_scalar_coefficient_scaleddiagonal. (exists pfa_gap_scalar_coefficient_scaleddiagonalbound. pfa_gap_scalar_coefficient_scaleddiagonalbound + S (pfc_index_scalar_coefficient_scaleddiagonal) = (S (i))) -> exists pfc_value_scalar_coefficient_scaleddiagonal. ((((exists ff_h_pfp_scalar_coefficient_scaleddiagonalentry. ff_h_pfp_scalar_coefficient_scaleddiagonalentry + S (pfc_value_scalar_coefficient_scaleddiagonal) = S ((S (pfc_index_scalar_coefficient_scaleddiagonal)) * pfc_terms_scale_scalar_coefficient_scaled)) /\ exists ff_q_pfp_scalar_coefficient_scaleddiagonalentry. pfc_terms_code_scalar_coefficient_scaled = ff_q_pfp_scalar_coefficient_scaleddiagonalentry * S ((S (pfc_index_scalar_coefficient_scaleddiagonal)) * pfc_terms_scale_scalar_coefficient_scaled) + (pfc_value_scalar_coefficient_scaleddiagonal))) /\ ((exists pfc_complement_scalar_coefficient_scaleddiagonalterm pfc_left_scalar_coefficient_scaleddiagonalterm pfc_right_scalar_coefficient_scaleddiagonalterm. (((pfc_index_scalar_coefficient_scaleddiagonal)+pfc_complement_scalar_coefficient_scaleddiagonalterm=(i)) /\ ((((((exists pfa_gap_scalar_coefficient_scaleddiagonaltermleftinside. pfa_gap_scalar_coefficient_scaleddiagonaltermleftinside + S (pfc_index_scalar_coefficient_scaleddiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_coefficient_scaleddiagonaltermleftentry. ff_h_pfp_scalar_coefficient_scaleddiagonaltermleftentry + S (pfc_left_scalar_coefficient_scaleddiagonalterm) = S ((S (pfc_index_scalar_coefficient_scaleddiagonal)) * ac)) /\ exists ff_q_pfp_scalar_coefficient_scaleddiagonaltermleftentry. ab = ff_q_pfp_scalar_coefficient_scaleddiagonaltermleftentry * S ((S (pfc_index_scalar_coefficient_scaleddiagonal)) * ac) + (pfc_left_scalar_coefficient_scaleddiagonalterm)))))) \/ (((exists pfc_gap_scalar_coefficient_scaleddiagonaltermleftoutside. pfc_gap_scalar_coefficient_scaleddiagonaltermleftoutside+(L)=(pfc_index_scalar_coefficient_scaleddiagonal)) /\ (((pfc_left_scalar_coefficient_scaleddiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_coefficient_scaleddiagonaltermrightinside. pfa_gap_scalar_coefficient_scaleddiagonaltermrightinside + S (pfc_complement_scalar_coefficient_scaleddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_coefficient_scaleddiagonaltermrightentry. ff_h_pfp_scalar_coefficient_scaleddiagonaltermrightentry + S (pfc_right_scalar_coefficient_scaleddiagonalterm) = S ((S (pfc_complement_scalar_coefficient_scaleddiagonalterm)) * sc)) /\ exists ff_q_pfp_scalar_coefficient_scaleddiagonaltermrightentry. sb = ff_q_pfp_scalar_coefficient_scaleddiagonaltermrightentry * S ((S (pfc_complement_scalar_coefficient_scaleddiagonalterm)) * sc) + (pfc_right_scalar_coefficient_scaleddiagonalterm)))))) \/ (((exists pfc_gap_scalar_coefficient_scaleddiagonaltermrightoutside. pfc_gap_scalar_coefficient_scaleddiagonaltermrightoutside+(M)=(pfc_complement_scalar_coefficient_scaleddiagonalterm)) /\ (((pfc_right_scalar_coefficient_scaleddiagonalterm)=0))))) /\ (((pfc_value_scalar_coefficient_scaleddiagonal)=pfc_left_scalar_coefficient_scaleddiagonalterm*pfc_right_scalar_coefficient_scaleddiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_coefficient_scaledsum fs_v_pfc_scalar_coefficient_scaledsum. ((((exists fs_h_pfc_scalar_coefficient_scaledsum_body_start. fs_h_pfc_scalar_coefficient_scaledsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_coefficient_scaledsum)) /\ exists fs_q_pfc_scalar_coefficient_scaledsum_body_start. fs_u_pfc_scalar_coefficient_scaledsum = fs_q_pfc_scalar_coefficient_scaledsum_body_start * S ((S (0)) * fs_v_pfc_scalar_coefficient_scaledsum) + (0))) /\ ((((exists fs_h_pfc_scalar_coefficient_scaledsum_body_terminal. fs_h_pfc_scalar_coefficient_scaledsum_body_terminal + S (pfc_natural_sum_scalar_coefficient_scaled) = S ((S (S (i))) * fs_v_pfc_scalar_coefficient_scaledsum)) /\ exists fs_q_pfc_scalar_coefficient_scaledsum_body_terminal. fs_u_pfc_scalar_coefficient_scaledsum = fs_q_pfc_scalar_coefficient_scaledsum_body_terminal * S ((S (S (i))) * fs_v_pfc_scalar_coefficient_scaledsum) + (pfc_natural_sum_scalar_coefficient_scaled))) /\ forall fs_i_pfc_scalar_coefficient_scaledsum_body_steps. (exists fs_lt_pfc_scalar_coefficient_scaledsum_body_steps_bound. fs_lt_pfc_scalar_coefficient_scaledsum_body_steps_bound + S fs_i_pfc_scalar_coefficient_scaledsum_body_steps = S (i)) -> exists fs_a_pfc_scalar_coefficient_scaledsum_body_steps fs_r_pfc_scalar_coefficient_scaledsum_body_steps fs_s_pfc_scalar_coefficient_scaledsum_body_steps. ((((exists fs_h_pfc_scalar_coefficient_scaledsum_body_steps_summand. fs_h_pfc_scalar_coefficient_scaledsum_body_steps_summand + S (fs_a_pfc_scalar_coefficient_scaledsum_body_steps) = S ((S (fs_i_pfc_scalar_coefficient_scaledsum_body_steps)) * pfc_terms_scale_scalar_coefficient_scaled)) /\ exists fs_q_pfc_scalar_coefficient_scaledsum_body_steps_summand. pfc_terms_code_scalar_coefficient_scaled = fs_q_pfc_scalar_coefficient_scaledsum_body_steps_summand * S ((S (fs_i_pfc_scalar_coefficient_scaledsum_body_steps)) * pfc_terms_scale_scalar_coefficient_scaled) + (fs_a_pfc_scalar_coefficient_scaledsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_coefficient_scaledsum_body_steps_partial. fs_h_pfc_scalar_coefficient_scaledsum_body_steps_partial + S (fs_r_pfc_scalar_coefficient_scaledsum_body_steps) = S ((S (fs_i_pfc_scalar_coefficient_scaledsum_body_steps)) * fs_v_pfc_scalar_coefficient_scaledsum)) /\ exists fs_q_pfc_scalar_coefficient_scaledsum_body_steps_partial. fs_u_pfc_scalar_coefficient_scaledsum = fs_q_pfc_scalar_coefficient_scaledsum_body_steps_partial * S ((S (fs_i_pfc_scalar_coefficient_scaledsum_body_steps)) * fs_v_pfc_scalar_coefficient_scaledsum) + (fs_r_pfc_scalar_coefficient_scaledsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_coefficient_scaledsum_body_steps_successor. fs_h_pfc_scalar_coefficient_scaledsum_body_steps_successor + S (fs_s_pfc_scalar_coefficient_scaledsum_body_steps) = S ((S (S fs_i_pfc_scalar_coefficient_scaledsum_body_steps)) * fs_v_pfc_scalar_coefficient_scaledsum)) /\ exists fs_q_pfc_scalar_coefficient_scaledsum_body_steps_successor. fs_u_pfc_scalar_coefficient_scaledsum = fs_q_pfc_scalar_coefficient_scaledsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_coefficient_scaledsum_body_steps)) * fs_v_pfc_scalar_coefficient_scaledsum) + (fs_s_pfc_scalar_coefficient_scaledsum_body_steps))) /\ fs_s_pfc_scalar_coefficient_scaledsum_body_steps = fs_r_pfc_scalar_coefficient_scaledsum_body_steps + fs_a_pfc_scalar_coefficient_scaledsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_coefficient_scaledresiduebound. pfa_gap_scalar_coefficient_scaledresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_scalar_coefficient_scaledresiduecongruence pfa_offset_right_scalar_coefficient_scaledresiduecongruence. (pfc_natural_sum_scalar_coefficient_scaled) + (p) * pfa_offset_left_scalar_coefficient_scaledresiduecongruence = (r) + (p) * pfa_offset_right_scalar_coefficient_scaledresiduecongruence))))))))) -> (((exists pfa_gap_scalar_coefficient_resultleft. pfa_gap_scalar_coefficient_resultleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_coefficient_resultright. pfa_gap_scalar_coefficient_resultright + S (c) = (p)) /\ ((((exists pfa_gap_scalar_coefficient_resultresultbound. pfa_gap_scalar_coefficient_resultresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_scalar_coefficient_resultresultcongruence pfa_offset_right_scalar_coefficient_resultresultcongruence. ((k) * (c)) + (p) * pfa_offset_left_scalar_coefficient_resultresultcongruence = (r) + (p) * pfa_offset_right_scalar_coefficient_resultresultcongruence)))))))))