prime_field_polynomial_convolution_left_padding_nonempty_right

forall p ab ac L bb bc M cb cc N BB BC t CB CC K. (~(p=0)) -> (~(L=0)) -> (~(M=0)) -> (((forall pfp_repeat_index_nonempty_factor_padding_rightzeros. (exists pfa_gap_nonempty_factor_padding_rightzerosindex. pfa_gap_nonempty_factor_padding_rightzerosindex + S (pfp_repeat_index_nonempty_factor_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_nonempty_factor_padding_rightzerosentry. ff_h_pfp_nonempty_factor_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_nonempty_factor_padding_rightzeros)) * BC)) /\ exists ff_q_pfp_nonempty_factor_padding_rightzerosentry. BB = ff_q_pfp_nonempty_factor_padding_rightzerosentry * S ((S (pfp_repeat_index_nonempty_factor_padding_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_nonempty_factor_padding_right pfrep_value_nonempty_factor_padding_right. (exists pfa_gap_nonempty_factor_padding_rightbound. pfa_gap_nonempty_factor_padding_rightbound + S (pfrep_index_nonempty_factor_padding_right) = (M)) -> (((exists ff_h_pfp_nonempty_factor_padding_rightinput. ff_h_pfp_nonempty_factor_padding_rightinput + S (pfrep_value_nonempty_factor_padding_right) = S ((S (pfrep_index_nonempty_factor_padding_right)) * bc)) /\ exists ff_q_pfp_nonempty_factor_padding_rightinput. bb = ff_q_pfp_nonempty_factor_padding_rightinput * S ((S (pfrep_index_nonempty_factor_padding_right)) * bc) + (pfrep_value_nonempty_factor_padding_right))) -> (((exists ff_h_pfp_nonempty_factor_padding_rightoutput. ff_h_pfp_nonempty_factor_padding_rightoutput + S (pfrep_value_nonempty_factor_padding_right) = S ((S ((t)+pfrep_index_nonempty_factor_padding_right)) * BC)) /\ exists ff_q_pfp_nonempty_factor_padding_rightoutput. BB = ff_q_pfp_nonempty_factor_padding_rightoutput * S ((S ((t)+pfrep_index_nonempty_factor_padding_right)) * BC) + (pfrep_value_nonempty_factor_padding_right))))))) -> (((forall fom_index_pfp_nonempty_old_rightleft. (exists fom_gap_pfp_nonempty_old_rightleft_index_bound. fom_gap_pfp_nonempty_old_rightleft_index_bound + S (fom_index_pfp_nonempty_old_rightleft) = L) -> exists fom_value_pfp_nonempty_old_rightleft. ((((exists fom_beta_height_pfp_nonempty_old_rightleft_entry. fom_beta_height_pfp_nonempty_old_rightleft_entry + S (fom_value_pfp_nonempty_old_rightleft) = S ((S (fom_index_pfp_nonempty_old_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_nonempty_old_rightleft_entry. ab = fom_beta_quotient_pfp_nonempty_old_rightleft_entry * S ((S (fom_index_pfp_nonempty_old_rightleft)) * ac) + (fom_value_pfp_nonempty_old_rightleft))) /\ (exists fom_gap_pfp_nonempty_old_rightleft_value_bound. fom_gap_pfp_nonempty_old_rightleft_value_bound + S (fom_value_pfp_nonempty_old_rightleft) = p))) /\ (((forall fom_index_pfp_nonempty_old_rightright. (exists fom_gap_pfp_nonempty_old_rightright_index_bound. fom_gap_pfp_nonempty_old_rightright_index_bound + S (fom_index_pfp_nonempty_old_rightright) = M) -> exists fom_value_pfp_nonempty_old_rightright. ((((exists fom_beta_height_pfp_nonempty_old_rightright_entry. fom_beta_height_pfp_nonempty_old_rightright_entry + S (fom_value_pfp_nonempty_old_rightright) = S ((S (fom_index_pfp_nonempty_old_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_nonempty_old_rightright_entry. bb = fom_beta_quotient_pfp_nonempty_old_rightright_entry * S ((S (fom_index_pfp_nonempty_old_rightright)) * bc) + (fom_value_pfp_nonempty_old_rightright))) /\ (exists fom_gap_pfp_nonempty_old_rightright_value_bound. fom_gap_pfp_nonempty_old_rightright_value_bound + S (fom_value_pfp_nonempty_old_rightright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_nonempty_old_rightcoefficients. (exists pfa_gap_nonempty_old_rightcoefficientsbound. pfa_gap_nonempty_old_rightcoefficientsbound + S (pfc_index_nonempty_old_rightcoefficients) = (N)) -> exists pfc_value_nonempty_old_rightcoefficients. ((((exists ff_h_pfp_nonempty_old_rightcoefficientsentry. ff_h_pfp_nonempty_old_rightcoefficientsentry + S (pfc_value_nonempty_old_rightcoefficients) = S ((S (pfc_index_nonempty_old_rightcoefficients)) * cc)) /\ exists ff_q_pfp_nonempty_old_rightcoefficientsentry. cb = ff_q_pfp_nonempty_old_rightcoefficientsentry * S ((S (pfc_index_nonempty_old_rightcoefficients)) * cc) + (pfc_value_nonempty_old_rightcoefficients))) /\ ((exists pfc_terms_code_nonempty_old_rightcoefficientscoefficient pfc_terms_scale_nonempty_old_rightcoefficientscoefficient pfc_natural_sum_nonempty_old_rightcoefficientscoefficient. ((forall pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal. (exists pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonalbound. pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonalbound + S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal) = (S (pfc_index_nonempty_old_rightcoefficients))) -> exists pfc_value_nonempty_old_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonalentry + S (pfc_value_nonempty_old_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_old_rightcoefficientscoefficient)) /\ exists ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_nonempty_old_rightcoefficientscoefficient = ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_old_rightcoefficientscoefficient) + (pfc_value_nonempty_old_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm. (((pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)+pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm=(pfc_index_nonempty_old_rightcoefficients)) /\ ((((((exists pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_nonempty_old_rightcoefficientscoefficientdiagonal)=pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm*pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_start. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_start. fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_nonempty_old_rightcoefficientscoefficient) = S ((S (S (pfc_index_nonempty_old_rightcoefficients))) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_nonempty_old_rightcoefficients))) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum) + (pfc_natural_sum_nonempty_old_rightcoefficientscoefficient))) /\ forall fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps = S (pfc_index_nonempty_old_rightcoefficients)) -> exists fs_a_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps fs_r_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps fs_s_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_old_rightcoefficientscoefficient)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_nonempty_old_rightcoefficientscoefficient = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_old_rightcoefficientscoefficient) + (fs_a_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum) + (fs_r_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum) + (fs_s_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_old_rightcoefficientscoefficientresiduebound. pfa_gap_nonempty_old_rightcoefficientscoefficientresiduebound + S (pfc_value_nonempty_old_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_nonempty_old_rightcoefficientscoefficientresiduecongruence pfa_offset_right_nonempty_old_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_nonempty_old_rightcoefficientscoefficient) + (p) * pfa_offset_left_nonempty_old_rightcoefficientscoefficientresiduecongruence = (pfc_value_nonempty_old_rightcoefficients) + (p) * pfa_offset_right_nonempty_old_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_nonempty_new_rightleft. (exists fom_gap_pfp_nonempty_new_rightleft_index_bound. fom_gap_pfp_nonempty_new_rightleft_index_bound + S (fom_index_pfp_nonempty_new_rightleft) = L) -> exists fom_value_pfp_nonempty_new_rightleft. ((((exists fom_beta_height_pfp_nonempty_new_rightleft_entry. fom_beta_height_pfp_nonempty_new_rightleft_entry + S (fom_value_pfp_nonempty_new_rightleft) = S ((S (fom_index_pfp_nonempty_new_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_nonempty_new_rightleft_entry. ab = fom_beta_quotient_pfp_nonempty_new_rightleft_entry * S ((S (fom_index_pfp_nonempty_new_rightleft)) * ac) + (fom_value_pfp_nonempty_new_rightleft))) /\ (exists fom_gap_pfp_nonempty_new_rightleft_value_bound. fom_gap_pfp_nonempty_new_rightleft_value_bound + S (fom_value_pfp_nonempty_new_rightleft) = p))) /\ (((forall fom_index_pfp_nonempty_new_rightright. (exists fom_gap_pfp_nonempty_new_rightright_index_bound. fom_gap_pfp_nonempty_new_rightright_index_bound + S (fom_index_pfp_nonempty_new_rightright) = t+M) -> exists fom_value_pfp_nonempty_new_rightright. ((((exists fom_beta_height_pfp_nonempty_new_rightright_entry. fom_beta_height_pfp_nonempty_new_rightright_entry + S (fom_value_pfp_nonempty_new_rightright) = S ((S (fom_index_pfp_nonempty_new_rightright)) * BC)) /\ exists fom_beta_quotient_pfp_nonempty_new_rightright_entry. BB = fom_beta_quotient_pfp_nonempty_new_rightright_entry * S ((S (fom_index_pfp_nonempty_new_rightright)) * BC) + (fom_value_pfp_nonempty_new_rightright))) /\ (exists fom_gap_pfp_nonempty_new_rightright_value_bound. fom_gap_pfp_nonempty_new_rightright_value_bound + S (fom_value_pfp_nonempty_new_rightright) = p))) /\ (((((((L)=0 \/ (t+M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((t+M)=0)) /\ (((L)+(t+M)=S (K)))))))) /\ ((forall pfc_index_nonempty_new_rightcoefficients. (exists pfa_gap_nonempty_new_rightcoefficientsbound. pfa_gap_nonempty_new_rightcoefficientsbound + S (pfc_index_nonempty_new_rightcoefficients) = (K)) -> exists pfc_value_nonempty_new_rightcoefficients. ((((exists ff_h_pfp_nonempty_new_rightcoefficientsentry. ff_h_pfp_nonempty_new_rightcoefficientsentry + S (pfc_value_nonempty_new_rightcoefficients) = S ((S (pfc_index_nonempty_new_rightcoefficients)) * CC)) /\ exists ff_q_pfp_nonempty_new_rightcoefficientsentry. CB = ff_q_pfp_nonempty_new_rightcoefficientsentry * S ((S (pfc_index_nonempty_new_rightcoefficients)) * CC) + (pfc_value_nonempty_new_rightcoefficients))) /\ ((exists pfc_terms_code_nonempty_new_rightcoefficientscoefficient pfc_terms_scale_nonempty_new_rightcoefficientscoefficient pfc_natural_sum_nonempty_new_rightcoefficientscoefficient. ((forall pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal. (exists pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonalbound. pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonalbound + S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal) = (S (pfc_index_nonempty_new_rightcoefficients))) -> exists pfc_value_nonempty_new_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonalentry + S (pfc_value_nonempty_new_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_new_rightcoefficientscoefficient)) /\ exists ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_nonempty_new_rightcoefficientscoefficient = ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_new_rightcoefficientscoefficient) + (pfc_value_nonempty_new_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm. (((pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)+pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm=(pfc_index_nonempty_new_rightcoefficients)) /\ ((((((exists pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermrightoutside+(t+M)=(pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_nonempty_new_rightcoefficientscoefficientdiagonal)=pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm*pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_start. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_start. fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_nonempty_new_rightcoefficientscoefficient) = S ((S (S (pfc_index_nonempty_new_rightcoefficients))) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_nonempty_new_rightcoefficients))) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum) + (pfc_natural_sum_nonempty_new_rightcoefficientscoefficient))) /\ forall fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps = S (pfc_index_nonempty_new_rightcoefficients)) -> exists fs_a_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps fs_r_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps fs_s_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_new_rightcoefficientscoefficient)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_nonempty_new_rightcoefficientscoefficient = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_new_rightcoefficientscoefficient) + (fs_a_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum) + (fs_r_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum) + (fs_s_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_new_rightcoefficientscoefficientresiduebound. pfa_gap_nonempty_new_rightcoefficientscoefficientresiduebound + S (pfc_value_nonempty_new_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_nonempty_new_rightcoefficientscoefficientresiduecongruence pfa_offset_right_nonempty_new_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_nonempty_new_rightcoefficientscoefficient) + (p) * pfa_offset_left_nonempty_new_rightcoefficientscoefficientresiduecongruence = (pfc_value_nonempty_new_rightcoefficients) + (p) * pfa_offset_right_nonempty_new_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((K=t+N) /\ ((((forall pfp_repeat_index_nonempty_product_padding_rightzeros. (exists pfa_gap_nonempty_product_padding_rightzerosindex. pfa_gap_nonempty_product_padding_rightzerosindex + S (pfp_repeat_index_nonempty_product_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_nonempty_product_padding_rightzerosentry. ff_h_pfp_nonempty_product_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_nonempty_product_padding_rightzeros)) * CC)) /\ exists ff_q_pfp_nonempty_product_padding_rightzerosentry. CB = ff_q_pfp_nonempty_product_padding_rightzerosentry * S ((S (pfp_repeat_index_nonempty_product_padding_rightzeros)) * CC) + (0)))) /\ ((forall pfrep_index_nonempty_product_padding_right pfrep_value_nonempty_product_padding_right. (exists pfa_gap_nonempty_product_padding_rightbound. pfa_gap_nonempty_product_padding_rightbound + S (pfrep_index_nonempty_product_padding_right) = (N)) -> (((exists ff_h_pfp_nonempty_product_padding_rightinput. ff_h_pfp_nonempty_product_padding_rightinput + S (pfrep_value_nonempty_product_padding_right) = S ((S (pfrep_index_nonempty_product_padding_right)) * cc)) /\ exists ff_q_pfp_nonempty_product_padding_rightinput. cb = ff_q_pfp_nonempty_product_padding_rightinput * S ((S (pfrep_index_nonempty_product_padding_right)) * cc) + (pfrep_value_nonempty_product_padding_right))) -> (((exists ff_h_pfp_nonempty_product_padding_rightoutput. ff_h_pfp_nonempty_product_padding_rightoutput + S (pfrep_value_nonempty_product_padding_right) = S ((S ((t)+pfrep_index_nonempty_product_padding_right)) * CC)) /\ exists ff_q_pfp_nonempty_product_padding_rightoutput. CB = ff_q_pfp_nonempty_product_padding_rightoutput * S ((S ((t)+pfrep_index_nonempty_product_padding_right)) * CC) + (pfrep_value_nonempty_product_padding_right))))))))))