prime_field_polynomial_convolution_right_scale

forall p k ab ac L bb bc M sb sc cb cc N db dc K. (((exists pfa_gap_scalar_product_inputscalar. pfa_gap_scalar_product_inputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_product_input. (exists pfa_gap_scalar_product_inputindex. pfa_gap_scalar_product_inputindex + S (pfp_index_scalar_product_input) = (M)) -> exists pfp_source_scalar_product_input pfp_value_scalar_product_input. ((((exists ff_h_pfp_scalar_product_inputsource. ff_h_pfp_scalar_product_inputsource + S (pfp_source_scalar_product_input) = S ((S (pfp_index_scalar_product_input)) * bc)) /\ exists ff_q_pfp_scalar_product_inputsource. bb = ff_q_pfp_scalar_product_inputsource * S ((S (pfp_index_scalar_product_input)) * bc) + (pfp_source_scalar_product_input))) /\ (((((exists ff_h_pfp_scalar_product_inputtarget. ff_h_pfp_scalar_product_inputtarget + S (pfp_value_scalar_product_input) = S ((S (pfp_index_scalar_product_input)) * sc)) /\ exists ff_q_pfp_scalar_product_inputtarget. sb = ff_q_pfp_scalar_product_inputtarget * S ((S (pfp_index_scalar_product_input)) * sc) + (pfp_value_scalar_product_input))) /\ ((((exists pfa_gap_scalar_product_inputoperationleft. pfa_gap_scalar_product_inputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_product_inputoperationright. pfa_gap_scalar_product_inputoperationright + S (pfp_source_scalar_product_input) = (p)) /\ ((((exists pfa_gap_scalar_product_inputoperationresultbound. pfa_gap_scalar_product_inputoperationresultbound + S (pfp_value_scalar_product_input) = (p)) /\ ((exists pfa_offset_left_scalar_product_inputoperationresultcongruence pfa_offset_right_scalar_product_inputoperationresultcongruence. ((k) * (pfp_source_scalar_product_input)) + (p) * pfa_offset_left_scalar_product_inputoperationresultcongruence = (pfp_value_scalar_product_input) + (p) * pfa_offset_right_scalar_product_inputoperationresultcongruence))))))))))))))))) -> (((forall fom_index_pfp_scalar_product_oldleft. (exists fom_gap_pfp_scalar_product_oldleft_index_bound. fom_gap_pfp_scalar_product_oldleft_index_bound + S (fom_index_pfp_scalar_product_oldleft) = L) -> exists fom_value_pfp_scalar_product_oldleft. ((((exists fom_beta_height_pfp_scalar_product_oldleft_entry. fom_beta_height_pfp_scalar_product_oldleft_entry + S (fom_value_pfp_scalar_product_oldleft) = S ((S (fom_index_pfp_scalar_product_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_product_oldleft_entry. ab = fom_beta_quotient_pfp_scalar_product_oldleft_entry * S ((S (fom_index_pfp_scalar_product_oldleft)) * ac) + (fom_value_pfp_scalar_product_oldleft))) /\ (exists fom_gap_pfp_scalar_product_oldleft_value_bound. fom_gap_pfp_scalar_product_oldleft_value_bound + S (fom_value_pfp_scalar_product_oldleft) = p))) /\ (((forall fom_index_pfp_scalar_product_oldright. (exists fom_gap_pfp_scalar_product_oldright_index_bound. fom_gap_pfp_scalar_product_oldright_index_bound + S (fom_index_pfp_scalar_product_oldright) = M) -> exists fom_value_pfp_scalar_product_oldright. ((((exists fom_beta_height_pfp_scalar_product_oldright_entry. fom_beta_height_pfp_scalar_product_oldright_entry + S (fom_value_pfp_scalar_product_oldright) = S ((S (fom_index_pfp_scalar_product_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_scalar_product_oldright_entry. bb = fom_beta_quotient_pfp_scalar_product_oldright_entry * S ((S (fom_index_pfp_scalar_product_oldright)) * bc) + (fom_value_pfp_scalar_product_oldright))) /\ (exists fom_gap_pfp_scalar_product_oldright_value_bound. fom_gap_pfp_scalar_product_oldright_value_bound + S (fom_value_pfp_scalar_product_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_product_oldcoefficients. (exists pfa_gap_scalar_product_oldcoefficientsbound. pfa_gap_scalar_product_oldcoefficientsbound + S (pfc_index_scalar_product_oldcoefficients) = (N)) -> exists pfc_value_scalar_product_oldcoefficients. ((((exists ff_h_pfp_scalar_product_oldcoefficientsentry. ff_h_pfp_scalar_product_oldcoefficientsentry + S (pfc_value_scalar_product_oldcoefficients) = S ((S (pfc_index_scalar_product_oldcoefficients)) * cc)) /\ exists ff_q_pfp_scalar_product_oldcoefficientsentry. cb = ff_q_pfp_scalar_product_oldcoefficientsentry * S ((S (pfc_index_scalar_product_oldcoefficients)) * cc) + (pfc_value_scalar_product_oldcoefficients))) /\ ((exists pfc_terms_code_scalar_product_oldcoefficientscoefficient pfc_terms_scale_scalar_product_oldcoefficientscoefficient pfc_natural_sum_scalar_product_oldcoefficientscoefficient. ((forall pfc_index_scalar_product_oldcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_product_oldcoefficientscoefficientdiagonalbound. pfa_gap_scalar_product_oldcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_product_oldcoefficients))) -> exists pfc_value_scalar_product_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_product_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_product_oldcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_product_oldcoefficientscoefficient = ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_product_oldcoefficientscoefficient) + (pfc_value_scalar_product_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)+pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm=(pfc_index_scalar_product_oldcoefficients)) /\ ((((((exists pfa_gap_scalar_product_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_product_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_product_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_product_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_product_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_product_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_product_oldcoefficientscoefficientdiagonal)=pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm*pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_product_oldcoefficientscoefficientsum fs_v_pfc_scalar_product_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_product_oldcoefficientscoefficientsum = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_product_oldcoefficientscoefficient) = S ((S (S (pfc_index_scalar_product_oldcoefficients))) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_product_oldcoefficientscoefficientsum = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_product_oldcoefficients))) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum) + (pfc_natural_sum_scalar_product_oldcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_product_oldcoefficients)) -> exists fs_a_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_product_oldcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_product_oldcoefficientscoefficient = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_product_oldcoefficientscoefficient) + (fs_a_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_product_oldcoefficientscoefficientsum = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum) + (fs_r_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_product_oldcoefficientscoefficientsum = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum) + (fs_s_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_product_oldcoefficientscoefficientresiduebound. pfa_gap_scalar_product_oldcoefficientscoefficientresiduebound + S (pfc_value_scalar_product_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_product_oldcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_product_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_product_oldcoefficientscoefficient) + (p) * pfa_offset_left_scalar_product_oldcoefficientscoefficientresiduecongruence = (pfc_value_scalar_product_oldcoefficients) + (p) * pfa_offset_right_scalar_product_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_scalar_product_scaledleft. (exists fom_gap_pfp_scalar_product_scaledleft_index_bound. fom_gap_pfp_scalar_product_scaledleft_index_bound + S (fom_index_pfp_scalar_product_scaledleft) = L) -> exists fom_value_pfp_scalar_product_scaledleft. ((((exists fom_beta_height_pfp_scalar_product_scaledleft_entry. fom_beta_height_pfp_scalar_product_scaledleft_entry + S (fom_value_pfp_scalar_product_scaledleft) = S ((S (fom_index_pfp_scalar_product_scaledleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_product_scaledleft_entry. ab = fom_beta_quotient_pfp_scalar_product_scaledleft_entry * S ((S (fom_index_pfp_scalar_product_scaledleft)) * ac) + (fom_value_pfp_scalar_product_scaledleft))) /\ (exists fom_gap_pfp_scalar_product_scaledleft_value_bound. fom_gap_pfp_scalar_product_scaledleft_value_bound + S (fom_value_pfp_scalar_product_scaledleft) = p))) /\ (((forall fom_index_pfp_scalar_product_scaledright. (exists fom_gap_pfp_scalar_product_scaledright_index_bound. fom_gap_pfp_scalar_product_scaledright_index_bound + S (fom_index_pfp_scalar_product_scaledright) = M) -> exists fom_value_pfp_scalar_product_scaledright. ((((exists fom_beta_height_pfp_scalar_product_scaledright_entry. fom_beta_height_pfp_scalar_product_scaledright_entry + S (fom_value_pfp_scalar_product_scaledright) = S ((S (fom_index_pfp_scalar_product_scaledright)) * sc)) /\ exists fom_beta_quotient_pfp_scalar_product_scaledright_entry. sb = fom_beta_quotient_pfp_scalar_product_scaledright_entry * S ((S (fom_index_pfp_scalar_product_scaledright)) * sc) + (fom_value_pfp_scalar_product_scaledright))) /\ (exists fom_gap_pfp_scalar_product_scaledright_value_bound. fom_gap_pfp_scalar_product_scaledright_value_bound + S (fom_value_pfp_scalar_product_scaledright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (K)))))))) /\ ((forall pfc_index_scalar_product_scaledcoefficients. (exists pfa_gap_scalar_product_scaledcoefficientsbound. pfa_gap_scalar_product_scaledcoefficientsbound + S (pfc_index_scalar_product_scaledcoefficients) = (K)) -> exists pfc_value_scalar_product_scaledcoefficients. ((((exists ff_h_pfp_scalar_product_scaledcoefficientsentry. ff_h_pfp_scalar_product_scaledcoefficientsentry + S (pfc_value_scalar_product_scaledcoefficients) = S ((S (pfc_index_scalar_product_scaledcoefficients)) * dc)) /\ exists ff_q_pfp_scalar_product_scaledcoefficientsentry. db = ff_q_pfp_scalar_product_scaledcoefficientsentry * S ((S (pfc_index_scalar_product_scaledcoefficients)) * dc) + (pfc_value_scalar_product_scaledcoefficients))) /\ ((exists pfc_terms_code_scalar_product_scaledcoefficientscoefficient pfc_terms_scale_scalar_product_scaledcoefficientscoefficient pfc_natural_sum_scalar_product_scaledcoefficientscoefficient. ((forall pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonalbound. pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_product_scaledcoefficients))) -> exists pfc_value_scalar_product_scaledcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_product_scaledcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_product_scaledcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_product_scaledcoefficientscoefficient = ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_product_scaledcoefficientscoefficient) + (pfc_value_scalar_product_scaledcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)+pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm=(pfc_index_scalar_product_scaledcoefficients)) /\ ((((((exists pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm)) * sc)) /\ exists ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermrightentry. sb = ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm)) * sc) + (pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_product_scaledcoefficientscoefficientdiagonal)=pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm*pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_product_scaledcoefficientscoefficient) = S ((S (S (pfc_index_scalar_product_scaledcoefficients))) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_product_scaledcoefficients))) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum) + (pfc_natural_sum_scalar_product_scaledcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_product_scaledcoefficients)) -> exists fs_a_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_product_scaledcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_product_scaledcoefficientscoefficient = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_product_scaledcoefficientscoefficient) + (fs_a_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum) + (fs_r_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum) + (fs_s_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_product_scaledcoefficientscoefficientresiduebound. pfa_gap_scalar_product_scaledcoefficientscoefficientresiduebound + S (pfc_value_scalar_product_scaledcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_product_scaledcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_product_scaledcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_product_scaledcoefficientscoefficient) + (p) * pfa_offset_left_scalar_product_scaledcoefficientscoefficientresiduecongruence = (pfc_value_scalar_product_scaledcoefficients) + (p) * pfa_offset_right_scalar_product_scaledcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((K=N) /\ ((((exists pfa_gap_scalar_product_resultscalar. pfa_gap_scalar_product_resultscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_product_result. (exists pfa_gap_scalar_product_resultindex. pfa_gap_scalar_product_resultindex + S (pfp_index_scalar_product_result) = (N)) -> exists pfp_source_scalar_product_result pfp_value_scalar_product_result. ((((exists ff_h_pfp_scalar_product_resultsource. ff_h_pfp_scalar_product_resultsource + S (pfp_source_scalar_product_result) = S ((S (pfp_index_scalar_product_result)) * cc)) /\ exists ff_q_pfp_scalar_product_resultsource. cb = ff_q_pfp_scalar_product_resultsource * S ((S (pfp_index_scalar_product_result)) * cc) + (pfp_source_scalar_product_result))) /\ (((((exists ff_h_pfp_scalar_product_resulttarget. ff_h_pfp_scalar_product_resulttarget + S (pfp_value_scalar_product_result) = S ((S (pfp_index_scalar_product_result)) * dc)) /\ exists ff_q_pfp_scalar_product_resulttarget. db = ff_q_pfp_scalar_product_resulttarget * S ((S (pfp_index_scalar_product_result)) * dc) + (pfp_value_scalar_product_result))) /\ ((((exists pfa_gap_scalar_product_resultoperationleft. pfa_gap_scalar_product_resultoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_product_resultoperationright. pfa_gap_scalar_product_resultoperationright + S (pfp_source_scalar_product_result) = (p)) /\ ((((exists pfa_gap_scalar_product_resultoperationresultbound. pfa_gap_scalar_product_resultoperationresultbound + S (pfp_value_scalar_product_result) = (p)) /\ ((exists pfa_offset_left_scalar_product_resultoperationresultcongruence pfa_offset_right_scalar_product_resultoperationresultcongruence. ((k) * (pfp_source_scalar_product_result)) + (p) * pfa_offset_left_scalar_product_resultoperationresultcongruence = (pfp_value_scalar_product_result) + (p) * pfa_offset_right_scalar_product_resultoperationresultcongruence))))))))))))))))))))