prime_field_polynomial_convolution_left_padding_nonempty_left

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M cb cc N AB AC t CB CC K. (~(p=0)) -> (~(L=0)) -> (~(M=0)) -> (((forall pfp_repeat_index_nonempty_factor_padding_leftzeros. (exists pfa_gap_nonempty_factor_padding_leftzerosindex. pfa_gap_nonempty_factor_padding_leftzerosindex + S (pfp_repeat_index_nonempty_factor_padding_leftzeros) = (t)) -> (((exists ff_h_pfp_nonempty_factor_padding_leftzerosentry. ff_h_pfp_nonempty_factor_padding_leftzerosentry + S (0) = S ((S (pfp_repeat_index_nonempty_factor_padding_leftzeros)) * AC)) /\ exists ff_q_pfp_nonempty_factor_padding_leftzerosentry. AB = ff_q_pfp_nonempty_factor_padding_leftzerosentry * S ((S (pfp_repeat_index_nonempty_factor_padding_leftzeros)) * AC) + (0)))) /\ ((forall pfrep_index_nonempty_factor_padding_left pfrep_value_nonempty_factor_padding_left. (exists pfa_gap_nonempty_factor_padding_leftbound. pfa_gap_nonempty_factor_padding_leftbound + S (pfrep_index_nonempty_factor_padding_left) = (L)) -> (((exists ff_h_pfp_nonempty_factor_padding_leftinput. ff_h_pfp_nonempty_factor_padding_leftinput + S (pfrep_value_nonempty_factor_padding_left) = S ((S (pfrep_index_nonempty_factor_padding_left)) * ac)) /\ exists ff_q_pfp_nonempty_factor_padding_leftinput. ab = ff_q_pfp_nonempty_factor_padding_leftinput * S ((S (pfrep_index_nonempty_factor_padding_left)) * ac) + (pfrep_value_nonempty_factor_padding_left))) -> (((exists ff_h_pfp_nonempty_factor_padding_leftoutput. ff_h_pfp_nonempty_factor_padding_leftoutput + S (pfrep_value_nonempty_factor_padding_left) = S ((S ((t)+pfrep_index_nonempty_factor_padding_left)) * AC)) /\ exists ff_q_pfp_nonempty_factor_padding_leftoutput. AB = ff_q_pfp_nonempty_factor_padding_leftoutput * S ((S ((t)+pfrep_index_nonempty_factor_padding_left)) * AC) + (pfrep_value_nonempty_factor_padding_left))))))) -> (((forall fom_index_pfp_nonempty_old_leftleft. (exists fom_gap_pfp_nonempty_old_leftleft_index_bound. fom_gap_pfp_nonempty_old_leftleft_index_bound + S (fom_index_pfp_nonempty_old_leftleft) = L) -> exists fom_value_pfp_nonempty_old_leftleft. ((((exists fom_beta_height_pfp_nonempty_old_leftleft_entry. fom_beta_height_pfp_nonempty_old_leftleft_entry + S (fom_value_pfp_nonempty_old_leftleft) = S ((S (fom_index_pfp_nonempty_old_leftleft)) * ac)) /\ exists fom_beta_quotient_pfp_nonempty_old_leftleft_entry. ab = fom_beta_quotient_pfp_nonempty_old_leftleft_entry * S ((S (fom_index_pfp_nonempty_old_leftleft)) * ac) + (fom_value_pfp_nonempty_old_leftleft))) /\ (exists fom_gap_pfp_nonempty_old_leftleft_value_bound. fom_gap_pfp_nonempty_old_leftleft_value_bound + S (fom_value_pfp_nonempty_old_leftleft) = p))) /\ (((forall fom_index_pfp_nonempty_old_leftright. (exists fom_gap_pfp_nonempty_old_leftright_index_bound. fom_gap_pfp_nonempty_old_leftright_index_bound + S (fom_index_pfp_nonempty_old_leftright) = M) -> exists fom_value_pfp_nonempty_old_leftright. ((((exists fom_beta_height_pfp_nonempty_old_leftright_entry. fom_beta_height_pfp_nonempty_old_leftright_entry + S (fom_value_pfp_nonempty_old_leftright) = S ((S (fom_index_pfp_nonempty_old_leftright)) * bc)) /\ exists fom_beta_quotient_pfp_nonempty_old_leftright_entry. bb = fom_beta_quotient_pfp_nonempty_old_leftright_entry * S ((S (fom_index_pfp_nonempty_old_leftright)) * bc) + (fom_value_pfp_nonempty_old_leftright))) /\ (exists fom_gap_pfp_nonempty_old_leftright_value_bound. fom_gap_pfp_nonempty_old_leftright_value_bound + S (fom_value_pfp_nonempty_old_leftright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_nonempty_old_leftcoefficients. (exists pfa_gap_nonempty_old_leftcoefficientsbound. pfa_gap_nonempty_old_leftcoefficientsbound + S (pfc_index_nonempty_old_leftcoefficients) = (N)) -> exists pfc_value_nonempty_old_leftcoefficients. ((((exists ff_h_pfp_nonempty_old_leftcoefficientsentry. ff_h_pfp_nonempty_old_leftcoefficientsentry + S (pfc_value_nonempty_old_leftcoefficients) = S ((S (pfc_index_nonempty_old_leftcoefficients)) * cc)) /\ exists ff_q_pfp_nonempty_old_leftcoefficientsentry. cb = ff_q_pfp_nonempty_old_leftcoefficientsentry * S ((S (pfc_index_nonempty_old_leftcoefficients)) * cc) + (pfc_value_nonempty_old_leftcoefficients))) /\ ((exists pfc_terms_code_nonempty_old_leftcoefficientscoefficient pfc_terms_scale_nonempty_old_leftcoefficientscoefficient pfc_natural_sum_nonempty_old_leftcoefficientscoefficient. ((forall pfc_index_nonempty_old_leftcoefficientscoefficientdiagonal. (exists pfa_gap_nonempty_old_leftcoefficientscoefficientdiagonalbound. pfa_gap_nonempty_old_leftcoefficientscoefficientdiagonalbound + S (pfc_index_nonempty_old_leftcoefficientscoefficientdiagonal) = (S (pfc_index_nonempty_old_leftcoefficients))) -> exists pfc_value_nonempty_old_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_nonempty_old_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_nonempty_old_leftcoefficientscoefficientdiagonalentry + S (pfc_value_nonempty_old_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_nonempty_old_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_old_leftcoefficientscoefficient)) /\ exists ff_q_pfp_nonempty_old_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_nonempty_old_leftcoefficientscoefficient = ff_q_pfp_nonempty_old_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_nonempty_old_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_old_leftcoefficientscoefficient) + (pfc_value_nonempty_old_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_nonempty_old_leftcoefficientscoefficientdiagonalterm pfc_left_nonempty_old_leftcoefficientscoefficientdiagonalterm pfc_right_nonempty_old_leftcoefficientscoefficientdiagonalterm. (((pfc_index_nonempty_old_leftcoefficientscoefficientdiagonal)+pfc_complement_nonempty_old_leftcoefficientscoefficientdiagonalterm=(pfc_index_nonempty_old_leftcoefficients)) /\ ((((((exists pfa_gap_nonempty_old_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_nonempty_old_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_nonempty_old_leftcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_nonempty_old_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_nonempty_old_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_nonempty_old_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_nonempty_old_leftcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_nonempty_old_leftcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_nonempty_old_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_nonempty_old_leftcoefficientscoefficientdiagonal)) * ac) + (pfc_left_nonempty_old_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_old_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_nonempty_old_leftcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_nonempty_old_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_nonempty_old_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_old_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_nonempty_old_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_nonempty_old_leftcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_nonempty_old_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_nonempty_old_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_nonempty_old_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_nonempty_old_leftcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_nonempty_old_leftcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_nonempty_old_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_nonempty_old_leftcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_nonempty_old_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_old_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_nonempty_old_leftcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_nonempty_old_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_nonempty_old_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_nonempty_old_leftcoefficientscoefficientdiagonal)=pfc_left_nonempty_old_leftcoefficientscoefficientdiagonalterm*pfc_right_nonempty_old_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_old_leftcoefficientscoefficientsum fs_v_pfc_nonempty_old_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_start. fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_old_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_start. fs_u_pfc_nonempty_old_leftcoefficientscoefficientsum = fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_old_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_nonempty_old_leftcoefficientscoefficient) = S ((S (S (pfc_index_nonempty_old_leftcoefficients))) * fs_v_pfc_nonempty_old_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_nonempty_old_leftcoefficientscoefficientsum = fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_nonempty_old_leftcoefficients))) * fs_v_pfc_nonempty_old_leftcoefficientscoefficientsum) + (pfc_natural_sum_nonempty_old_leftcoefficientscoefficient))) /\ forall fs_i_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps = S (pfc_index_nonempty_old_leftcoefficients)) -> exists fs_a_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps fs_r_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps fs_s_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_old_leftcoefficientscoefficient)) /\ exists fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_nonempty_old_leftcoefficientscoefficient = fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_old_leftcoefficientscoefficient) + (fs_a_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_nonempty_old_leftcoefficientscoefficientsum = fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_leftcoefficientscoefficientsum) + (fs_r_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_nonempty_old_leftcoefficientscoefficientsum = fs_q_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_leftcoefficientscoefficientsum) + (fs_s_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_nonempty_old_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_old_leftcoefficientscoefficientresiduebound. pfa_gap_nonempty_old_leftcoefficientscoefficientresiduebound + S (pfc_value_nonempty_old_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_nonempty_old_leftcoefficientscoefficientresiduecongruence pfa_offset_right_nonempty_old_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_nonempty_old_leftcoefficientscoefficient) + (p) * pfa_offset_left_nonempty_old_leftcoefficientscoefficientresiduecongruence = (pfc_value_nonempty_old_leftcoefficients) + (p) * pfa_offset_right_nonempty_old_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_nonempty_new_leftleft. (exists fom_gap_pfp_nonempty_new_leftleft_index_bound. fom_gap_pfp_nonempty_new_leftleft_index_bound + S (fom_index_pfp_nonempty_new_leftleft) = t+L) -> exists fom_value_pfp_nonempty_new_leftleft. ((((exists fom_beta_height_pfp_nonempty_new_leftleft_entry. fom_beta_height_pfp_nonempty_new_leftleft_entry + S (fom_value_pfp_nonempty_new_leftleft) = S ((S (fom_index_pfp_nonempty_new_leftleft)) * AC)) /\ exists fom_beta_quotient_pfp_nonempty_new_leftleft_entry. AB = fom_beta_quotient_pfp_nonempty_new_leftleft_entry * S ((S (fom_index_pfp_nonempty_new_leftleft)) * AC) + (fom_value_pfp_nonempty_new_leftleft))) /\ (exists fom_gap_pfp_nonempty_new_leftleft_value_bound. fom_gap_pfp_nonempty_new_leftleft_value_bound + S (fom_value_pfp_nonempty_new_leftleft) = p))) /\ (((forall fom_index_pfp_nonempty_new_leftright. (exists fom_gap_pfp_nonempty_new_leftright_index_bound. fom_gap_pfp_nonempty_new_leftright_index_bound + S (fom_index_pfp_nonempty_new_leftright) = M) -> exists fom_value_pfp_nonempty_new_leftright. ((((exists fom_beta_height_pfp_nonempty_new_leftright_entry. fom_beta_height_pfp_nonempty_new_leftright_entry + S (fom_value_pfp_nonempty_new_leftright) = S ((S (fom_index_pfp_nonempty_new_leftright)) * bc)) /\ exists fom_beta_quotient_pfp_nonempty_new_leftright_entry. bb = fom_beta_quotient_pfp_nonempty_new_leftright_entry * S ((S (fom_index_pfp_nonempty_new_leftright)) * bc) + (fom_value_pfp_nonempty_new_leftright))) /\ (exists fom_gap_pfp_nonempty_new_leftright_value_bound. fom_gap_pfp_nonempty_new_leftright_value_bound + S (fom_value_pfp_nonempty_new_leftright) = p))) /\ (((((((t+L)=0 \/ (M)=0) /\ (((K)=0)))) \/ (((~((t+L)=0)) /\ (((~((M)=0)) /\ (((t+L)+(M)=S (K)))))))) /\ ((forall pfc_index_nonempty_new_leftcoefficients. (exists pfa_gap_nonempty_new_leftcoefficientsbound. pfa_gap_nonempty_new_leftcoefficientsbound + S (pfc_index_nonempty_new_leftcoefficients) = (K)) -> exists pfc_value_nonempty_new_leftcoefficients. ((((exists ff_h_pfp_nonempty_new_leftcoefficientsentry. ff_h_pfp_nonempty_new_leftcoefficientsentry + S (pfc_value_nonempty_new_leftcoefficients) = S ((S (pfc_index_nonempty_new_leftcoefficients)) * CC)) /\ exists ff_q_pfp_nonempty_new_leftcoefficientsentry. CB = ff_q_pfp_nonempty_new_leftcoefficientsentry * S ((S (pfc_index_nonempty_new_leftcoefficients)) * CC) + (pfc_value_nonempty_new_leftcoefficients))) /\ ((exists pfc_terms_code_nonempty_new_leftcoefficientscoefficient pfc_terms_scale_nonempty_new_leftcoefficientscoefficient pfc_natural_sum_nonempty_new_leftcoefficientscoefficient. ((forall pfc_index_nonempty_new_leftcoefficientscoefficientdiagonal. (exists pfa_gap_nonempty_new_leftcoefficientscoefficientdiagonalbound. pfa_gap_nonempty_new_leftcoefficientscoefficientdiagonalbound + S (pfc_index_nonempty_new_leftcoefficientscoefficientdiagonal) = (S (pfc_index_nonempty_new_leftcoefficients))) -> exists pfc_value_nonempty_new_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_nonempty_new_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_nonempty_new_leftcoefficientscoefficientdiagonalentry + S (pfc_value_nonempty_new_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_nonempty_new_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_new_leftcoefficientscoefficient)) /\ exists ff_q_pfp_nonempty_new_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_nonempty_new_leftcoefficientscoefficient = ff_q_pfp_nonempty_new_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_nonempty_new_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_new_leftcoefficientscoefficient) + (pfc_value_nonempty_new_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_nonempty_new_leftcoefficientscoefficientdiagonalterm pfc_left_nonempty_new_leftcoefficientscoefficientdiagonalterm pfc_right_nonempty_new_leftcoefficientscoefficientdiagonalterm. (((pfc_index_nonempty_new_leftcoefficientscoefficientdiagonal)+pfc_complement_nonempty_new_leftcoefficientscoefficientdiagonalterm=(pfc_index_nonempty_new_leftcoefficients)) /\ ((((((exists pfa_gap_nonempty_new_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_nonempty_new_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_nonempty_new_leftcoefficientscoefficientdiagonal) = (t+L)) /\ ((((exists ff_h_pfp_nonempty_new_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_nonempty_new_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_nonempty_new_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_nonempty_new_leftcoefficientscoefficientdiagonal)) * AC)) /\ exists ff_q_pfp_nonempty_new_leftcoefficientscoefficientdiagonaltermleftentry. AB = ff_q_pfp_nonempty_new_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_nonempty_new_leftcoefficientscoefficientdiagonal)) * AC) + (pfc_left_nonempty_new_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_new_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_nonempty_new_leftcoefficientscoefficientdiagonaltermleftoutside+(t+L)=(pfc_index_nonempty_new_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_nonempty_new_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_new_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_nonempty_new_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_nonempty_new_leftcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_nonempty_new_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_nonempty_new_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_nonempty_new_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_nonempty_new_leftcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_nonempty_new_leftcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_nonempty_new_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_nonempty_new_leftcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_nonempty_new_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_new_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_nonempty_new_leftcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_nonempty_new_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_nonempty_new_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_nonempty_new_leftcoefficientscoefficientdiagonal)=pfc_left_nonempty_new_leftcoefficientscoefficientdiagonalterm*pfc_right_nonempty_new_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_new_leftcoefficientscoefficientsum fs_v_pfc_nonempty_new_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_start. fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_new_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_start. fs_u_pfc_nonempty_new_leftcoefficientscoefficientsum = fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_new_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_nonempty_new_leftcoefficientscoefficient) = S ((S (S (pfc_index_nonempty_new_leftcoefficients))) * fs_v_pfc_nonempty_new_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_nonempty_new_leftcoefficientscoefficientsum = fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_nonempty_new_leftcoefficients))) * fs_v_pfc_nonempty_new_leftcoefficientscoefficientsum) + (pfc_natural_sum_nonempty_new_leftcoefficientscoefficient))) /\ forall fs_i_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps = S (pfc_index_nonempty_new_leftcoefficients)) -> exists fs_a_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps fs_r_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps fs_s_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_new_leftcoefficientscoefficient)) /\ exists fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_nonempty_new_leftcoefficientscoefficient = fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_new_leftcoefficientscoefficient) + (fs_a_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_nonempty_new_leftcoefficientscoefficientsum = fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_leftcoefficientscoefficientsum) + (fs_r_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_nonempty_new_leftcoefficientscoefficientsum = fs_q_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_leftcoefficientscoefficientsum) + (fs_s_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_nonempty_new_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_new_leftcoefficientscoefficientresiduebound. pfa_gap_nonempty_new_leftcoefficientscoefficientresiduebound + S (pfc_value_nonempty_new_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_nonempty_new_leftcoefficientscoefficientresiduecongruence pfa_offset_right_nonempty_new_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_nonempty_new_leftcoefficientscoefficient) + (p) * pfa_offset_left_nonempty_new_leftcoefficientscoefficientresiduecongruence = (pfc_value_nonempty_new_leftcoefficients) + (p) * pfa_offset_right_nonempty_new_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((K=t+N) /\ ((((forall pfp_repeat_index_nonempty_product_padding_leftzeros. (exists pfa_gap_nonempty_product_padding_leftzerosindex. pfa_gap_nonempty_product_padding_leftzerosindex + S (pfp_repeat_index_nonempty_product_padding_leftzeros) = (t)) -> (((exists ff_h_pfp_nonempty_product_padding_leftzerosentry. ff_h_pfp_nonempty_product_padding_leftzerosentry + S (0) = S ((S (pfp_repeat_index_nonempty_product_padding_leftzeros)) * CC)) /\ exists ff_q_pfp_nonempty_product_padding_leftzerosentry. CB = ff_q_pfp_nonempty_product_padding_leftzerosentry * S ((S (pfp_repeat_index_nonempty_product_padding_leftzeros)) * CC) + (0)))) /\ ((forall pfrep_index_nonempty_product_padding_left pfrep_value_nonempty_product_padding_left. (exists pfa_gap_nonempty_product_padding_leftbound. pfa_gap_nonempty_product_padding_leftbound + S (pfrep_index_nonempty_product_padding_left) = (N)) -> (((exists ff_h_pfp_nonempty_product_padding_leftinput. ff_h_pfp_nonempty_product_padding_leftinput + S (pfrep_value_nonempty_product_padding_left) = S ((S (pfrep_index_nonempty_product_padding_left)) * cc)) /\ exists ff_q_pfp_nonempty_product_padding_leftinput. cb = ff_q_pfp_nonempty_product_padding_leftinput * S ((S (pfrep_index_nonempty_product_padding_left)) * cc) + (pfrep_value_nonempty_product_padding_left))) -> (((exists ff_h_pfp_nonempty_product_padding_leftoutput. ff_h_pfp_nonempty_product_padding_leftoutput + S (pfrep_value_nonempty_product_padding_left) = S ((S ((t)+pfrep_index_nonempty_product_padding_left)) * CC)) /\ exists ff_q_pfp_nonempty_product_padding_leftoutput. CB = ff_q_pfp_nonempty_product_padding_leftoutput * S ((S ((t)+pfrep_index_nonempty_product_padding_left)) * CC) + (pfrep_value_nonempty_product_padding_left))))))))))