prime_field_polynomial_convolution_right_scale_exists

forall p k ab ac L bb bc M cb cc N. (~(p=0)) -> (exists pfa_gap_scalar_exists_scalar. pfa_gap_scalar_exists_scalar + S (k) = (p)) -> (((forall fom_index_pfp_scalar_exists_originalleft. (exists fom_gap_pfp_scalar_exists_originalleft_index_bound. fom_gap_pfp_scalar_exists_originalleft_index_bound + S (fom_index_pfp_scalar_exists_originalleft) = L) -> exists fom_value_pfp_scalar_exists_originalleft. ((((exists fom_beta_height_pfp_scalar_exists_originalleft_entry. fom_beta_height_pfp_scalar_exists_originalleft_entry + S (fom_value_pfp_scalar_exists_originalleft) = S ((S (fom_index_pfp_scalar_exists_originalleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_exists_originalleft_entry. ab = fom_beta_quotient_pfp_scalar_exists_originalleft_entry * S ((S (fom_index_pfp_scalar_exists_originalleft)) * ac) + (fom_value_pfp_scalar_exists_originalleft))) /\ (exists fom_gap_pfp_scalar_exists_originalleft_value_bound. fom_gap_pfp_scalar_exists_originalleft_value_bound + S (fom_value_pfp_scalar_exists_originalleft) = p))) /\ (((forall fom_index_pfp_scalar_exists_originalright. (exists fom_gap_pfp_scalar_exists_originalright_index_bound. fom_gap_pfp_scalar_exists_originalright_index_bound + S (fom_index_pfp_scalar_exists_originalright) = M) -> exists fom_value_pfp_scalar_exists_originalright. ((((exists fom_beta_height_pfp_scalar_exists_originalright_entry. fom_beta_height_pfp_scalar_exists_originalright_entry + S (fom_value_pfp_scalar_exists_originalright) = S ((S (fom_index_pfp_scalar_exists_originalright)) * bc)) /\ exists fom_beta_quotient_pfp_scalar_exists_originalright_entry. bb = fom_beta_quotient_pfp_scalar_exists_originalright_entry * S ((S (fom_index_pfp_scalar_exists_originalright)) * bc) + (fom_value_pfp_scalar_exists_originalright))) /\ (exists fom_gap_pfp_scalar_exists_originalright_value_bound. fom_gap_pfp_scalar_exists_originalright_value_bound + S (fom_value_pfp_scalar_exists_originalright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_exists_originalcoefficients. (exists pfa_gap_scalar_exists_originalcoefficientsbound. pfa_gap_scalar_exists_originalcoefficientsbound + S (pfc_index_scalar_exists_originalcoefficients) = (N)) -> exists pfc_value_scalar_exists_originalcoefficients. ((((exists ff_h_pfp_scalar_exists_originalcoefficientsentry. ff_h_pfp_scalar_exists_originalcoefficientsentry + S (pfc_value_scalar_exists_originalcoefficients) = S ((S (pfc_index_scalar_exists_originalcoefficients)) * cc)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientsentry. cb = ff_q_pfp_scalar_exists_originalcoefficientsentry * S ((S (pfc_index_scalar_exists_originalcoefficients)) * cc) + (pfc_value_scalar_exists_originalcoefficients))) /\ ((exists pfc_terms_code_scalar_exists_originalcoefficientscoefficient pfc_terms_scale_scalar_exists_originalcoefficientscoefficient pfc_natural_sum_scalar_exists_originalcoefficientscoefficient. ((forall pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonalbound. pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_exists_originalcoefficients))) -> exists pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_exists_originalcoefficientscoefficient = ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient) + (pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)+pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm=(pfc_index_scalar_exists_originalcoefficients)) /\ ((((((exists pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal)=pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm*pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_exists_originalcoefficientscoefficient) = S ((S (S (pfc_index_scalar_exists_originalcoefficients))) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_exists_originalcoefficients))) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (pfc_natural_sum_scalar_exists_originalcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_exists_originalcoefficients)) -> exists fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_exists_originalcoefficientscoefficient = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient) + (fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_exists_originalcoefficientscoefficientresiduebound. pfa_gap_scalar_exists_originalcoefficientscoefficientresiduebound + S (pfc_value_scalar_exists_originalcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_exists_originalcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_exists_originalcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_exists_originalcoefficientscoefficient) + (p) * pfa_offset_left_scalar_exists_originalcoefficientscoefficientresiduecongruence = (pfc_value_scalar_exists_originalcoefficients) + (p) * pfa_offset_right_scalar_exists_originalcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (exists sb sc db dc eb ec. ((((exists pfa_gap_scalar_exists_inputscalar. pfa_gap_scalar_exists_inputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_exists_input. (exists pfa_gap_scalar_exists_inputindex. pfa_gap_scalar_exists_inputindex + S (pfp_index_scalar_exists_input) = (M)) -> exists pfp_source_scalar_exists_input pfp_value_scalar_exists_input. ((((exists ff_h_pfp_scalar_exists_inputsource. ff_h_pfp_scalar_exists_inputsource + S (pfp_source_scalar_exists_input) = S ((S (pfp_index_scalar_exists_input)) * bc)) /\ exists ff_q_pfp_scalar_exists_inputsource. bb = ff_q_pfp_scalar_exists_inputsource * S ((S (pfp_index_scalar_exists_input)) * bc) + (pfp_source_scalar_exists_input))) /\ (((((exists ff_h_pfp_scalar_exists_inputtarget. ff_h_pfp_scalar_exists_inputtarget + S (pfp_value_scalar_exists_input) = S ((S (pfp_index_scalar_exists_input)) * sc)) /\ exists ff_q_pfp_scalar_exists_inputtarget. sb = ff_q_pfp_scalar_exists_inputtarget * S ((S (pfp_index_scalar_exists_input)) * sc) + (pfp_value_scalar_exists_input))) /\ ((((exists pfa_gap_scalar_exists_inputoperationleft. pfa_gap_scalar_exists_inputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_exists_inputoperationright. pfa_gap_scalar_exists_inputoperationright + S (pfp_source_scalar_exists_input) = (p)) /\ ((((exists pfa_gap_scalar_exists_inputoperationresultbound. pfa_gap_scalar_exists_inputoperationresultbound + S (pfp_value_scalar_exists_input) = (p)) /\ ((exists pfa_offset_left_scalar_exists_inputoperationresultcongruence pfa_offset_right_scalar_exists_inputoperationresultcongruence. ((k) * (pfp_source_scalar_exists_input)) + (p) * pfa_offset_left_scalar_exists_inputoperationresultcongruence = (pfp_value_scalar_exists_input) + (p) * pfa_offset_right_scalar_exists_inputoperationresultcongruence))))))))))))))))) /\ (((((forall fom_index_pfp_scalar_exists_newleft. (exists fom_gap_pfp_scalar_exists_newleft_index_bound. fom_gap_pfp_scalar_exists_newleft_index_bound + S (fom_index_pfp_scalar_exists_newleft) = L) -> exists fom_value_pfp_scalar_exists_newleft. ((((exists fom_beta_height_pfp_scalar_exists_newleft_entry. fom_beta_height_pfp_scalar_exists_newleft_entry + S (fom_value_pfp_scalar_exists_newleft) = S ((S (fom_index_pfp_scalar_exists_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_exists_newleft_entry. ab = fom_beta_quotient_pfp_scalar_exists_newleft_entry * S ((S (fom_index_pfp_scalar_exists_newleft)) * ac) + (fom_value_pfp_scalar_exists_newleft))) /\ (exists fom_gap_pfp_scalar_exists_newleft_value_bound. fom_gap_pfp_scalar_exists_newleft_value_bound + S (fom_value_pfp_scalar_exists_newleft) = p))) /\ (((forall fom_index_pfp_scalar_exists_newright. (exists fom_gap_pfp_scalar_exists_newright_index_bound. fom_gap_pfp_scalar_exists_newright_index_bound + S (fom_index_pfp_scalar_exists_newright) = M) -> exists fom_value_pfp_scalar_exists_newright. ((((exists fom_beta_height_pfp_scalar_exists_newright_entry. fom_beta_height_pfp_scalar_exists_newright_entry + S (fom_value_pfp_scalar_exists_newright) = S ((S (fom_index_pfp_scalar_exists_newright)) * sc)) /\ exists fom_beta_quotient_pfp_scalar_exists_newright_entry. sb = fom_beta_quotient_pfp_scalar_exists_newright_entry * S ((S (fom_index_pfp_scalar_exists_newright)) * sc) + (fom_value_pfp_scalar_exists_newright))) /\ (exists fom_gap_pfp_scalar_exists_newright_value_bound. fom_gap_pfp_scalar_exists_newright_value_bound + S (fom_value_pfp_scalar_exists_newright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_exists_newcoefficients. (exists pfa_gap_scalar_exists_newcoefficientsbound. pfa_gap_scalar_exists_newcoefficientsbound + S (pfc_index_scalar_exists_newcoefficients) = (N)) -> exists pfc_value_scalar_exists_newcoefficients. ((((exists ff_h_pfp_scalar_exists_newcoefficientsentry. ff_h_pfp_scalar_exists_newcoefficientsentry + S (pfc_value_scalar_exists_newcoefficients) = S ((S (pfc_index_scalar_exists_newcoefficients)) * dc)) /\ exists ff_q_pfp_scalar_exists_newcoefficientsentry. db = ff_q_pfp_scalar_exists_newcoefficientsentry * S ((S (pfc_index_scalar_exists_newcoefficients)) * dc) + (pfc_value_scalar_exists_newcoefficients))) /\ ((exists pfc_terms_code_scalar_exists_newcoefficientscoefficient pfc_terms_scale_scalar_exists_newcoefficientscoefficient pfc_natural_sum_scalar_exists_newcoefficientscoefficient. ((forall pfc_index_scalar_exists_newcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_exists_newcoefficientscoefficientdiagonalbound. pfa_gap_scalar_exists_newcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_exists_newcoefficients))) -> exists pfc_value_scalar_exists_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_exists_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_newcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_exists_newcoefficientscoefficient = ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_newcoefficientscoefficient) + (pfc_value_scalar_exists_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)+pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm=(pfc_index_scalar_exists_newcoefficients)) /\ ((((((exists pfa_gap_scalar_exists_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_exists_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_exists_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_exists_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_exists_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm)) * sc)) /\ exists ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermrightentry. sb = ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm)) * sc) + (pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_exists_newcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_exists_newcoefficientscoefficientdiagonal)=pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm*pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_exists_newcoefficientscoefficientsum fs_v_pfc_scalar_exists_newcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_exists_newcoefficientscoefficientsum = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_exists_newcoefficientscoefficient) = S ((S (S (pfc_index_scalar_exists_newcoefficients))) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_exists_newcoefficientscoefficientsum = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_exists_newcoefficients))) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum) + (pfc_natural_sum_scalar_exists_newcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_exists_newcoefficients)) -> exists fs_a_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_newcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_exists_newcoefficientscoefficient = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_newcoefficientscoefficient) + (fs_a_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_exists_newcoefficientscoefficientsum = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum) + (fs_r_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_exists_newcoefficientscoefficientsum = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum) + (fs_s_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_exists_newcoefficientscoefficientresiduebound. pfa_gap_scalar_exists_newcoefficientscoefficientresiduebound + S (pfc_value_scalar_exists_newcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_exists_newcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_exists_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_exists_newcoefficientscoefficient) + (p) * pfa_offset_left_scalar_exists_newcoefficientscoefficientresiduecongruence = (pfc_value_scalar_exists_newcoefficients) + (p) * pfa_offset_right_scalar_exists_newcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((exists pfa_gap_scalar_exists_outputscalar. pfa_gap_scalar_exists_outputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_exists_output. (exists pfa_gap_scalar_exists_outputindex. pfa_gap_scalar_exists_outputindex + S (pfp_index_scalar_exists_output) = (N)) -> exists pfp_source_scalar_exists_output pfp_value_scalar_exists_output. ((((exists ff_h_pfp_scalar_exists_outputsource. ff_h_pfp_scalar_exists_outputsource + S (pfp_source_scalar_exists_output) = S ((S (pfp_index_scalar_exists_output)) * cc)) /\ exists ff_q_pfp_scalar_exists_outputsource. cb = ff_q_pfp_scalar_exists_outputsource * S ((S (pfp_index_scalar_exists_output)) * cc) + (pfp_source_scalar_exists_output))) /\ (((((exists ff_h_pfp_scalar_exists_outputtarget. ff_h_pfp_scalar_exists_outputtarget + S (pfp_value_scalar_exists_output) = S ((S (pfp_index_scalar_exists_output)) * ec)) /\ exists ff_q_pfp_scalar_exists_outputtarget. eb = ff_q_pfp_scalar_exists_outputtarget * S ((S (pfp_index_scalar_exists_output)) * ec) + (pfp_value_scalar_exists_output))) /\ ((((exists pfa_gap_scalar_exists_outputoperationleft. pfa_gap_scalar_exists_outputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_exists_outputoperationright. pfa_gap_scalar_exists_outputoperationright + S (pfp_source_scalar_exists_output) = (p)) /\ ((((exists pfa_gap_scalar_exists_outputoperationresultbound. pfa_gap_scalar_exists_outputoperationresultbound + S (pfp_value_scalar_exists_output) = (p)) /\ ((exists pfa_offset_left_scalar_exists_outputoperationresultcongruence pfa_offset_right_scalar_exists_outputoperationresultcongruence. ((k) * (pfp_source_scalar_exists_output)) + (p) * pfa_offset_left_scalar_exists_outputoperationresultcongruence = (pfp_value_scalar_exists_output) + (p) * pfa_offset_right_scalar_exists_outputoperationresultcongruence))))))))))))))))) /\ ((forall mdr_i_pfp_scalar_exists_equal mdr_a_pfp_scalar_exists_equal. (exists mdr_gap_pfp_scalar_exists_equalb. mdr_gap_pfp_scalar_exists_equalb + S (mdr_i_pfp_scalar_exists_equal) = (N)) -> (((exists ff_h_mdr_pfp_scalar_exists_equalo. ff_h_mdr_pfp_scalar_exists_equalo + S (mdr_a_pfp_scalar_exists_equal) = S ((S (mdr_i_pfp_scalar_exists_equal)) * dc)) /\ exists ff_q_mdr_pfp_scalar_exists_equalo. db = ff_q_mdr_pfp_scalar_exists_equalo * S ((S (mdr_i_pfp_scalar_exists_equal)) * dc) + (mdr_a_pfp_scalar_exists_equal))) -> (((exists ff_h_mdr_pfp_scalar_exists_equaln. ff_h_mdr_pfp_scalar_exists_equaln + S (mdr_a_pfp_scalar_exists_equal) = S ((S (mdr_i_pfp_scalar_exists_equal)) * ec)) /\ exists ff_q_mdr_pfp_scalar_exists_equaln. eb = ff_q_mdr_pfp_scalar_exists_equaln * S ((S (mdr_i_pfp_scalar_exists_equal)) * ec) + (mdr_a_pfp_scalar_exists_equal)))))))))))