prime_field_convolution_coefficient_right_append_add

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M c db dc kb kc tb tc i u v w. (~((p) = 1) /\ forall pfa_factor_left_append_coefficient_prime pfa_factor_right_append_coefficient_prime. (p) = pfa_factor_left_append_coefficient_prime * pfa_factor_right_append_coefficient_prime -> pfa_factor_left_append_coefficient_prime = 1 \/ pfa_factor_right_append_coefficient_prime = 1) -> (forall fom_index_pfp_append_coefficient_old_coefficients. (exists fom_gap_pfp_append_coefficient_old_coefficients_index_bound. fom_gap_pfp_append_coefficient_old_coefficients_index_bound + S (fom_index_pfp_append_coefficient_old_coefficients) = M) -> exists fom_value_pfp_append_coefficient_old_coefficients. ((((exists fom_beta_height_pfp_append_coefficient_old_coefficients_entry. fom_beta_height_pfp_append_coefficient_old_coefficients_entry + S (fom_value_pfp_append_coefficient_old_coefficients) = S ((S (fom_index_pfp_append_coefficient_old_coefficients)) * bc)) /\ exists fom_beta_quotient_pfp_append_coefficient_old_coefficients_entry. bb = fom_beta_quotient_pfp_append_coefficient_old_coefficients_entry * S ((S (fom_index_pfp_append_coefficient_old_coefficients)) * bc) + (fom_value_pfp_append_coefficient_old_coefficients))) /\ (exists fom_gap_pfp_append_coefficient_old_coefficients_value_bound. fom_gap_pfp_append_coefficient_old_coefficients_value_bound + S (fom_value_pfp_append_coefficient_old_coefficients) = p))) -> (exists pfa_gap_append_coefficient_scalar. pfa_gap_append_coefficient_scalar + S (c) = (p)) -> (forall mdr_i_pfp_append_coefficient_preserve mdr_a_pfp_append_coefficient_preserve. (exists mdr_gap_pfp_append_coefficient_preserveb. mdr_gap_pfp_append_coefficient_preserveb + S (mdr_i_pfp_append_coefficient_preserve) = (M)) -> (((exists ff_h_mdr_pfp_append_coefficient_preserveo. ff_h_mdr_pfp_append_coefficient_preserveo + S (mdr_a_pfp_append_coefficient_preserve) = S ((S (mdr_i_pfp_append_coefficient_preserve)) * bc)) /\ exists ff_q_mdr_pfp_append_coefficient_preserveo. bb = ff_q_mdr_pfp_append_coefficient_preserveo * S ((S (mdr_i_pfp_append_coefficient_preserve)) * bc) + (mdr_a_pfp_append_coefficient_preserve))) -> (((exists ff_h_mdr_pfp_append_coefficient_preserven. ff_h_mdr_pfp_append_coefficient_preserven + S (mdr_a_pfp_append_coefficient_preserve) = S ((S (mdr_i_pfp_append_coefficient_preserve)) * dc)) /\ exists ff_q_mdr_pfp_append_coefficient_preserven. db = ff_q_mdr_pfp_append_coefficient_preserven * S ((S (mdr_i_pfp_append_coefficient_preserve)) * dc) + (mdr_a_pfp_append_coefficient_preserve)))) -> (((exists ff_h_pfp_append_coefficient_actual_last. ff_h_pfp_append_coefficient_actual_last + S (c) = S ((S (M)) * dc)) /\ exists ff_q_pfp_append_coefficient_actual_last. db = ff_q_pfp_append_coefficient_actual_last * S ((S (M)) * dc) + (c))) -> (((exists ff_h_pfp_append_coefficient_singleton. ff_h_pfp_append_coefficient_singleton + S (c) = S ((S (0)) * kc)) /\ exists ff_q_pfp_append_coefficient_singleton. kb = ff_q_pfp_append_coefficient_singleton * S ((S (0)) * kc) + (c))) -> (((forall pfp_repeat_index_append_coefficient_padzeros. (exists pfa_gap_append_coefficient_padzerosindex. pfa_gap_append_coefficient_padzerosindex + S (pfp_repeat_index_append_coefficient_padzeros) = (M)) -> (((exists ff_h_pfp_append_coefficient_padzerosentry. ff_h_pfp_append_coefficient_padzerosentry + S (0) = S ((S (pfp_repeat_index_append_coefficient_padzeros)) * tc)) /\ exists ff_q_pfp_append_coefficient_padzerosentry. tb = ff_q_pfp_append_coefficient_padzerosentry * S ((S (pfp_repeat_index_append_coefficient_padzeros)) * tc) + (0)))) /\ ((forall pfrep_index_append_coefficient_pad pfrep_value_append_coefficient_pad. (exists pfa_gap_append_coefficient_padbound. pfa_gap_append_coefficient_padbound + S (pfrep_index_append_coefficient_pad) = (1)) -> (((exists ff_h_pfp_append_coefficient_padinput. ff_h_pfp_append_coefficient_padinput + S (pfrep_value_append_coefficient_pad) = S ((S (pfrep_index_append_coefficient_pad)) * kc)) /\ exists ff_q_pfp_append_coefficient_padinput. kb = ff_q_pfp_append_coefficient_padinput * S ((S (pfrep_index_append_coefficient_pad)) * kc) + (pfrep_value_append_coefficient_pad))) -> (((exists ff_h_pfp_append_coefficient_padoutput. ff_h_pfp_append_coefficient_padoutput + S (pfrep_value_append_coefficient_pad) = S ((S ((M)+pfrep_index_append_coefficient_pad)) * tc)) /\ exists ff_q_pfp_append_coefficient_padoutput. tb = ff_q_pfp_append_coefficient_padoutput * S ((S ((M)+pfrep_index_append_coefficient_pad)) * tc) + (pfrep_value_append_coefficient_pad))))))) -> (exists pfc_terms_code_append_coefficient_old pfc_terms_scale_append_coefficient_old pfc_natural_sum_append_coefficient_old. ((forall pfc_index_append_coefficient_olddiagonal. (exists pfa_gap_append_coefficient_olddiagonalbound. pfa_gap_append_coefficient_olddiagonalbound + S (pfc_index_append_coefficient_olddiagonal) = (S (i))) -> exists pfc_value_append_coefficient_olddiagonal. ((((exists ff_h_pfp_append_coefficient_olddiagonalentry. ff_h_pfp_append_coefficient_olddiagonalentry + S (pfc_value_append_coefficient_olddiagonal) = S ((S (pfc_index_append_coefficient_olddiagonal)) * pfc_terms_scale_append_coefficient_old)) /\ exists ff_q_pfp_append_coefficient_olddiagonalentry. pfc_terms_code_append_coefficient_old = ff_q_pfp_append_coefficient_olddiagonalentry * S ((S (pfc_index_append_coefficient_olddiagonal)) * pfc_terms_scale_append_coefficient_old) + (pfc_value_append_coefficient_olddiagonal))) /\ ((exists pfc_complement_append_coefficient_olddiagonalterm pfc_left_append_coefficient_olddiagonalterm pfc_right_append_coefficient_olddiagonalterm. (((pfc_index_append_coefficient_olddiagonal)+pfc_complement_append_coefficient_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_append_coefficient_olddiagonaltermleftinside. pfa_gap_append_coefficient_olddiagonaltermleftinside + S (pfc_index_append_coefficient_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_append_coefficient_olddiagonaltermleftentry. ff_h_pfp_append_coefficient_olddiagonaltermleftentry + S (pfc_left_append_coefficient_olddiagonalterm) = S ((S (pfc_index_append_coefficient_olddiagonal)) * ac)) /\ exists ff_q_pfp_append_coefficient_olddiagonaltermleftentry. ab = ff_q_pfp_append_coefficient_olddiagonaltermleftentry * S ((S (pfc_index_append_coefficient_olddiagonal)) * ac) + (pfc_left_append_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_olddiagonaltermleftoutside. pfc_gap_append_coefficient_olddiagonaltermleftoutside+(L)=(pfc_index_append_coefficient_olddiagonal)) /\ (((pfc_left_append_coefficient_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_coefficient_olddiagonaltermrightinside. pfa_gap_append_coefficient_olddiagonaltermrightinside + S (pfc_complement_append_coefficient_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_append_coefficient_olddiagonaltermrightentry. ff_h_pfp_append_coefficient_olddiagonaltermrightentry + S (pfc_right_append_coefficient_olddiagonalterm) = S ((S (pfc_complement_append_coefficient_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_append_coefficient_olddiagonaltermrightentry. bb = ff_q_pfp_append_coefficient_olddiagonaltermrightentry * S ((S (pfc_complement_append_coefficient_olddiagonalterm)) * bc) + (pfc_right_append_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_olddiagonaltermrightoutside. pfc_gap_append_coefficient_olddiagonaltermrightoutside+(M)=(pfc_complement_append_coefficient_olddiagonalterm)) /\ (((pfc_right_append_coefficient_olddiagonalterm)=0))))) /\ (((pfc_value_append_coefficient_olddiagonal)=pfc_left_append_coefficient_olddiagonalterm*pfc_right_append_coefficient_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_coefficient_oldsum fs_v_pfc_append_coefficient_oldsum. ((((exists fs_h_pfc_append_coefficient_oldsum_body_start. fs_h_pfc_append_coefficient_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_coefficient_oldsum)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_start. fs_u_pfc_append_coefficient_oldsum = fs_q_pfc_append_coefficient_oldsum_body_start * S ((S (0)) * fs_v_pfc_append_coefficient_oldsum) + (0))) /\ ((((exists fs_h_pfc_append_coefficient_oldsum_body_terminal. fs_h_pfc_append_coefficient_oldsum_body_terminal + S (pfc_natural_sum_append_coefficient_old) = S ((S (S (i))) * fs_v_pfc_append_coefficient_oldsum)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_terminal. fs_u_pfc_append_coefficient_oldsum = fs_q_pfc_append_coefficient_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_append_coefficient_oldsum) + (pfc_natural_sum_append_coefficient_old))) /\ forall fs_i_pfc_append_coefficient_oldsum_body_steps. (exists fs_lt_pfc_append_coefficient_oldsum_body_steps_bound. fs_lt_pfc_append_coefficient_oldsum_body_steps_bound + S fs_i_pfc_append_coefficient_oldsum_body_steps = S (i)) -> exists fs_a_pfc_append_coefficient_oldsum_body_steps fs_r_pfc_append_coefficient_oldsum_body_steps fs_s_pfc_append_coefficient_oldsum_body_steps. ((((exists fs_h_pfc_append_coefficient_oldsum_body_steps_summand. fs_h_pfc_append_coefficient_oldsum_body_steps_summand + S (fs_a_pfc_append_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_oldsum_body_steps)) * pfc_terms_scale_append_coefficient_old)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_steps_summand. pfc_terms_code_append_coefficient_old = fs_q_pfc_append_coefficient_oldsum_body_steps_summand * S ((S (fs_i_pfc_append_coefficient_oldsum_body_steps)) * pfc_terms_scale_append_coefficient_old) + (fs_a_pfc_append_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_oldsum_body_steps_partial. fs_h_pfc_append_coefficient_oldsum_body_steps_partial + S (fs_r_pfc_append_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_oldsum_body_steps)) * fs_v_pfc_append_coefficient_oldsum)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_steps_partial. fs_u_pfc_append_coefficient_oldsum = fs_q_pfc_append_coefficient_oldsum_body_steps_partial * S ((S (fs_i_pfc_append_coefficient_oldsum_body_steps)) * fs_v_pfc_append_coefficient_oldsum) + (fs_r_pfc_append_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_oldsum_body_steps_successor. fs_h_pfc_append_coefficient_oldsum_body_steps_successor + S (fs_s_pfc_append_coefficient_oldsum_body_steps) = S ((S (S fs_i_pfc_append_coefficient_oldsum_body_steps)) * fs_v_pfc_append_coefficient_oldsum)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_steps_successor. fs_u_pfc_append_coefficient_oldsum = fs_q_pfc_append_coefficient_oldsum_body_steps_successor * S ((S (S fs_i_pfc_append_coefficient_oldsum_body_steps)) * fs_v_pfc_append_coefficient_oldsum) + (fs_s_pfc_append_coefficient_oldsum_body_steps))) /\ fs_s_pfc_append_coefficient_oldsum_body_steps = fs_r_pfc_append_coefficient_oldsum_body_steps + fs_a_pfc_append_coefficient_oldsum_body_steps)))))) /\ ((((exists pfa_gap_append_coefficient_oldresiduebound. pfa_gap_append_coefficient_oldresiduebound + S (u) = (p)) /\ ((exists pfa_offset_left_append_coefficient_oldresiduecongruence pfa_offset_right_append_coefficient_oldresiduecongruence. (pfc_natural_sum_append_coefficient_old) + (p) * pfa_offset_left_append_coefficient_oldresiduecongruence = (u) + (p) * pfa_offset_right_append_coefficient_oldresiduecongruence))))))))) -> (exists pfc_terms_code_append_coefficient_constant pfc_terms_scale_append_coefficient_constant pfc_natural_sum_append_coefficient_constant. ((forall pfc_index_append_coefficient_constantdiagonal. (exists pfa_gap_append_coefficient_constantdiagonalbound. pfa_gap_append_coefficient_constantdiagonalbound + S (pfc_index_append_coefficient_constantdiagonal) = (S (i))) -> exists pfc_value_append_coefficient_constantdiagonal. ((((exists ff_h_pfp_append_coefficient_constantdiagonalentry. ff_h_pfp_append_coefficient_constantdiagonalentry + S (pfc_value_append_coefficient_constantdiagonal) = S ((S (pfc_index_append_coefficient_constantdiagonal)) * pfc_terms_scale_append_coefficient_constant)) /\ exists ff_q_pfp_append_coefficient_constantdiagonalentry. pfc_terms_code_append_coefficient_constant = ff_q_pfp_append_coefficient_constantdiagonalentry * S ((S (pfc_index_append_coefficient_constantdiagonal)) * pfc_terms_scale_append_coefficient_constant) + (pfc_value_append_coefficient_constantdiagonal))) /\ ((exists pfc_complement_append_coefficient_constantdiagonalterm pfc_left_append_coefficient_constantdiagonalterm pfc_right_append_coefficient_constantdiagonalterm. (((pfc_index_append_coefficient_constantdiagonal)+pfc_complement_append_coefficient_constantdiagonalterm=(i)) /\ ((((((exists pfa_gap_append_coefficient_constantdiagonaltermleftinside. pfa_gap_append_coefficient_constantdiagonaltermleftinside + S (pfc_index_append_coefficient_constantdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_coefficient_constantdiagonaltermleftentry. ff_h_pfp_append_coefficient_constantdiagonaltermleftentry + S (pfc_left_append_coefficient_constantdiagonalterm) = S ((S (pfc_index_append_coefficient_constantdiagonal)) * ac)) /\ exists ff_q_pfp_append_coefficient_constantdiagonaltermleftentry. ab = ff_q_pfp_append_coefficient_constantdiagonaltermleftentry * S ((S (pfc_index_append_coefficient_constantdiagonal)) * ac) + (pfc_left_append_coefficient_constantdiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_constantdiagonaltermleftoutside. pfc_gap_append_coefficient_constantdiagonaltermleftoutside+(L)=(pfc_index_append_coefficient_constantdiagonal)) /\ (((pfc_left_append_coefficient_constantdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_coefficient_constantdiagonaltermrightinside. pfa_gap_append_coefficient_constantdiagonaltermrightinside + S (pfc_complement_append_coefficient_constantdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_append_coefficient_constantdiagonaltermrightentry. ff_h_pfp_append_coefficient_constantdiagonaltermrightentry + S (pfc_right_append_coefficient_constantdiagonalterm) = S ((S (pfc_complement_append_coefficient_constantdiagonalterm)) * tc)) /\ exists ff_q_pfp_append_coefficient_constantdiagonaltermrightentry. tb = ff_q_pfp_append_coefficient_constantdiagonaltermrightentry * S ((S (pfc_complement_append_coefficient_constantdiagonalterm)) * tc) + (pfc_right_append_coefficient_constantdiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_constantdiagonaltermrightoutside. pfc_gap_append_coefficient_constantdiagonaltermrightoutside+(S M)=(pfc_complement_append_coefficient_constantdiagonalterm)) /\ (((pfc_right_append_coefficient_constantdiagonalterm)=0))))) /\ (((pfc_value_append_coefficient_constantdiagonal)=pfc_left_append_coefficient_constantdiagonalterm*pfc_right_append_coefficient_constantdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_coefficient_constantsum fs_v_pfc_append_coefficient_constantsum. ((((exists fs_h_pfc_append_coefficient_constantsum_body_start. fs_h_pfc_append_coefficient_constantsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_coefficient_constantsum)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_start. fs_u_pfc_append_coefficient_constantsum = fs_q_pfc_append_coefficient_constantsum_body_start * S ((S (0)) * fs_v_pfc_append_coefficient_constantsum) + (0))) /\ ((((exists fs_h_pfc_append_coefficient_constantsum_body_terminal. fs_h_pfc_append_coefficient_constantsum_body_terminal + S (pfc_natural_sum_append_coefficient_constant) = S ((S (S (i))) * fs_v_pfc_append_coefficient_constantsum)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_terminal. fs_u_pfc_append_coefficient_constantsum = fs_q_pfc_append_coefficient_constantsum_body_terminal * S ((S (S (i))) * fs_v_pfc_append_coefficient_constantsum) + (pfc_natural_sum_append_coefficient_constant))) /\ forall fs_i_pfc_append_coefficient_constantsum_body_steps. (exists fs_lt_pfc_append_coefficient_constantsum_body_steps_bound. fs_lt_pfc_append_coefficient_constantsum_body_steps_bound + S fs_i_pfc_append_coefficient_constantsum_body_steps = S (i)) -> exists fs_a_pfc_append_coefficient_constantsum_body_steps fs_r_pfc_append_coefficient_constantsum_body_steps fs_s_pfc_append_coefficient_constantsum_body_steps. ((((exists fs_h_pfc_append_coefficient_constantsum_body_steps_summand. fs_h_pfc_append_coefficient_constantsum_body_steps_summand + S (fs_a_pfc_append_coefficient_constantsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_constantsum_body_steps)) * pfc_terms_scale_append_coefficient_constant)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_steps_summand. pfc_terms_code_append_coefficient_constant = fs_q_pfc_append_coefficient_constantsum_body_steps_summand * S ((S (fs_i_pfc_append_coefficient_constantsum_body_steps)) * pfc_terms_scale_append_coefficient_constant) + (fs_a_pfc_append_coefficient_constantsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_constantsum_body_steps_partial. fs_h_pfc_append_coefficient_constantsum_body_steps_partial + S (fs_r_pfc_append_coefficient_constantsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_constantsum_body_steps)) * fs_v_pfc_append_coefficient_constantsum)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_steps_partial. fs_u_pfc_append_coefficient_constantsum = fs_q_pfc_append_coefficient_constantsum_body_steps_partial * S ((S (fs_i_pfc_append_coefficient_constantsum_body_steps)) * fs_v_pfc_append_coefficient_constantsum) + (fs_r_pfc_append_coefficient_constantsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_constantsum_body_steps_successor. fs_h_pfc_append_coefficient_constantsum_body_steps_successor + S (fs_s_pfc_append_coefficient_constantsum_body_steps) = S ((S (S fs_i_pfc_append_coefficient_constantsum_body_steps)) * fs_v_pfc_append_coefficient_constantsum)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_steps_successor. fs_u_pfc_append_coefficient_constantsum = fs_q_pfc_append_coefficient_constantsum_body_steps_successor * S ((S (S fs_i_pfc_append_coefficient_constantsum_body_steps)) * fs_v_pfc_append_coefficient_constantsum) + (fs_s_pfc_append_coefficient_constantsum_body_steps))) /\ fs_s_pfc_append_coefficient_constantsum_body_steps = fs_r_pfc_append_coefficient_constantsum_body_steps + fs_a_pfc_append_coefficient_constantsum_body_steps)))))) /\ ((((exists pfa_gap_append_coefficient_constantresiduebound. pfa_gap_append_coefficient_constantresiduebound + S (v) = (p)) /\ ((exists pfa_offset_left_append_coefficient_constantresiduecongruence pfa_offset_right_append_coefficient_constantresiduecongruence. (pfc_natural_sum_append_coefficient_constant) + (p) * pfa_offset_left_append_coefficient_constantresiduecongruence = (v) + (p) * pfa_offset_right_append_coefficient_constantresiduecongruence))))))))) -> (exists pfc_terms_code_append_coefficient_new pfc_terms_scale_append_coefficient_new pfc_natural_sum_append_coefficient_new. ((forall pfc_index_append_coefficient_newdiagonal. (exists pfa_gap_append_coefficient_newdiagonalbound. pfa_gap_append_coefficient_newdiagonalbound + S (pfc_index_append_coefficient_newdiagonal) = (S (i))) -> exists pfc_value_append_coefficient_newdiagonal. ((((exists ff_h_pfp_append_coefficient_newdiagonalentry. ff_h_pfp_append_coefficient_newdiagonalentry + S (pfc_value_append_coefficient_newdiagonal) = S ((S (pfc_index_append_coefficient_newdiagonal)) * pfc_terms_scale_append_coefficient_new)) /\ exists ff_q_pfp_append_coefficient_newdiagonalentry. pfc_terms_code_append_coefficient_new = ff_q_pfp_append_coefficient_newdiagonalentry * S ((S (pfc_index_append_coefficient_newdiagonal)) * pfc_terms_scale_append_coefficient_new) + (pfc_value_append_coefficient_newdiagonal))) /\ ((exists pfc_complement_append_coefficient_newdiagonalterm pfc_left_append_coefficient_newdiagonalterm pfc_right_append_coefficient_newdiagonalterm. (((pfc_index_append_coefficient_newdiagonal)+pfc_complement_append_coefficient_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_append_coefficient_newdiagonaltermleftinside. pfa_gap_append_coefficient_newdiagonaltermleftinside + S (pfc_index_append_coefficient_newdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_coefficient_newdiagonaltermleftentry. ff_h_pfp_append_coefficient_newdiagonaltermleftentry + S (pfc_left_append_coefficient_newdiagonalterm) = S ((S (pfc_index_append_coefficient_newdiagonal)) * ac)) /\ exists ff_q_pfp_append_coefficient_newdiagonaltermleftentry. ab = ff_q_pfp_append_coefficient_newdiagonaltermleftentry * S ((S (pfc_index_append_coefficient_newdiagonal)) * ac) + (pfc_left_append_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_newdiagonaltermleftoutside. pfc_gap_append_coefficient_newdiagonaltermleftoutside+(L)=(pfc_index_append_coefficient_newdiagonal)) /\ (((pfc_left_append_coefficient_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_coefficient_newdiagonaltermrightinside. pfa_gap_append_coefficient_newdiagonaltermrightinside + S (pfc_complement_append_coefficient_newdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_append_coefficient_newdiagonaltermrightentry. ff_h_pfp_append_coefficient_newdiagonaltermrightentry + S (pfc_right_append_coefficient_newdiagonalterm) = S ((S (pfc_complement_append_coefficient_newdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_coefficient_newdiagonaltermrightentry. db = ff_q_pfp_append_coefficient_newdiagonaltermrightentry * S ((S (pfc_complement_append_coefficient_newdiagonalterm)) * dc) + (pfc_right_append_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_newdiagonaltermrightoutside. pfc_gap_append_coefficient_newdiagonaltermrightoutside+(S M)=(pfc_complement_append_coefficient_newdiagonalterm)) /\ (((pfc_right_append_coefficient_newdiagonalterm)=0))))) /\ (((pfc_value_append_coefficient_newdiagonal)=pfc_left_append_coefficient_newdiagonalterm*pfc_right_append_coefficient_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_coefficient_newsum fs_v_pfc_append_coefficient_newsum. ((((exists fs_h_pfc_append_coefficient_newsum_body_start. fs_h_pfc_append_coefficient_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_coefficient_newsum)) /\ exists fs_q_pfc_append_coefficient_newsum_body_start. fs_u_pfc_append_coefficient_newsum = fs_q_pfc_append_coefficient_newsum_body_start * S ((S (0)) * fs_v_pfc_append_coefficient_newsum) + (0))) /\ ((((exists fs_h_pfc_append_coefficient_newsum_body_terminal. fs_h_pfc_append_coefficient_newsum_body_terminal + S (pfc_natural_sum_append_coefficient_new) = S ((S (S (i))) * fs_v_pfc_append_coefficient_newsum)) /\ exists fs_q_pfc_append_coefficient_newsum_body_terminal. fs_u_pfc_append_coefficient_newsum = fs_q_pfc_append_coefficient_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_append_coefficient_newsum) + (pfc_natural_sum_append_coefficient_new))) /\ forall fs_i_pfc_append_coefficient_newsum_body_steps. (exists fs_lt_pfc_append_coefficient_newsum_body_steps_bound. fs_lt_pfc_append_coefficient_newsum_body_steps_bound + S fs_i_pfc_append_coefficient_newsum_body_steps = S (i)) -> exists fs_a_pfc_append_coefficient_newsum_body_steps fs_r_pfc_append_coefficient_newsum_body_steps fs_s_pfc_append_coefficient_newsum_body_steps. ((((exists fs_h_pfc_append_coefficient_newsum_body_steps_summand. fs_h_pfc_append_coefficient_newsum_body_steps_summand + S (fs_a_pfc_append_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_newsum_body_steps)) * pfc_terms_scale_append_coefficient_new)) /\ exists fs_q_pfc_append_coefficient_newsum_body_steps_summand. pfc_terms_code_append_coefficient_new = fs_q_pfc_append_coefficient_newsum_body_steps_summand * S ((S (fs_i_pfc_append_coefficient_newsum_body_steps)) * pfc_terms_scale_append_coefficient_new) + (fs_a_pfc_append_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_newsum_body_steps_partial. fs_h_pfc_append_coefficient_newsum_body_steps_partial + S (fs_r_pfc_append_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_newsum_body_steps)) * fs_v_pfc_append_coefficient_newsum)) /\ exists fs_q_pfc_append_coefficient_newsum_body_steps_partial. fs_u_pfc_append_coefficient_newsum = fs_q_pfc_append_coefficient_newsum_body_steps_partial * S ((S (fs_i_pfc_append_coefficient_newsum_body_steps)) * fs_v_pfc_append_coefficient_newsum) + (fs_r_pfc_append_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_newsum_body_steps_successor. fs_h_pfc_append_coefficient_newsum_body_steps_successor + S (fs_s_pfc_append_coefficient_newsum_body_steps) = S ((S (S fs_i_pfc_append_coefficient_newsum_body_steps)) * fs_v_pfc_append_coefficient_newsum)) /\ exists fs_q_pfc_append_coefficient_newsum_body_steps_successor. fs_u_pfc_append_coefficient_newsum = fs_q_pfc_append_coefficient_newsum_body_steps_successor * S ((S (S fs_i_pfc_append_coefficient_newsum_body_steps)) * fs_v_pfc_append_coefficient_newsum) + (fs_s_pfc_append_coefficient_newsum_body_steps))) /\ fs_s_pfc_append_coefficient_newsum_body_steps = fs_r_pfc_append_coefficient_newsum_body_steps + fs_a_pfc_append_coefficient_newsum_body_steps)))))) /\ ((((exists pfa_gap_append_coefficient_newresiduebound. pfa_gap_append_coefficient_newresiduebound + S (w) = (p)) /\ ((exists pfa_offset_left_append_coefficient_newresiduecongruence pfa_offset_right_append_coefficient_newresiduecongruence. (pfc_natural_sum_append_coefficient_new) + (p) * pfa_offset_left_append_coefficient_newresiduecongruence = (w) + (p) * pfa_offset_right_append_coefficient_newresiduecongruence))))))))) -> (((exists pfa_gap_append_coefficient_resultleft. pfa_gap_append_coefficient_resultleft + S (u) = (p)) /\ (((exists pfa_gap_append_coefficient_resultright. pfa_gap_append_coefficient_resultright + S (v) = (p)) /\ ((((exists pfa_gap_append_coefficient_resultresultbound. pfa_gap_append_coefficient_resultresultbound + S (w) = (p)) /\ ((exists pfa_offset_left_append_coefficient_resultresultcongruence pfa_offset_right_append_coefficient_resultresultcongruence. ((u) + (v)) + (p) * pfa_offset_left_append_coefficient_resultresultcongruence = (w) + (p) * pfa_offset_right_append_coefficient_resultresultcongruence)))))))))