prime_field_polynomial_division_residual_data_functional

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc d qb qc QB QC q pb pc ub uc t rb rc R PB PC UB UC T RB RC K. (forall mdr_i_pfp_residual_unique_quotients mdr_a_pfp_residual_unique_quotients. (exists mdr_gap_pfp_residual_unique_quotientsb. mdr_gap_pfp_residual_unique_quotientsb + S (mdr_i_pfp_residual_unique_quotients) = (q)) -> (((exists ff_h_mdr_pfp_residual_unique_quotientso. ff_h_mdr_pfp_residual_unique_quotientso + S (mdr_a_pfp_residual_unique_quotients) = S ((S (mdr_i_pfp_residual_unique_quotients)) * qc)) /\ exists ff_q_mdr_pfp_residual_unique_quotientso. qb = ff_q_mdr_pfp_residual_unique_quotientso * S ((S (mdr_i_pfp_residual_unique_quotients)) * qc) + (mdr_a_pfp_residual_unique_quotients))) -> (((exists ff_h_mdr_pfp_residual_unique_quotientsn. ff_h_mdr_pfp_residual_unique_quotientsn + S (mdr_a_pfp_residual_unique_quotients) = S ((S (mdr_i_pfp_residual_unique_quotients)) * QC)) /\ exists ff_q_mdr_pfp_residual_unique_quotientsn. QB = ff_q_mdr_pfp_residual_unique_quotientsn * S ((S (mdr_i_pfp_residual_unique_quotients)) * QC) + (mdr_a_pfp_residual_unique_quotients)))) -> (((forall pfc_index_residual_unique_firstproduct. (exists pfa_gap_residual_unique_firstproductbound. pfa_gap_residual_unique_firstproductbound + S (pfc_index_residual_unique_firstproduct) = (L)) -> exists pfc_value_residual_unique_firstproduct. ((((exists ff_h_pfp_residual_unique_firstproductentry. ff_h_pfp_residual_unique_firstproductentry + S (pfc_value_residual_unique_firstproduct) = S ((S (pfc_index_residual_unique_firstproduct)) * pc)) /\ exists ff_q_pfp_residual_unique_firstproductentry. pb = ff_q_pfp_residual_unique_firstproductentry * S ((S (pfc_index_residual_unique_firstproduct)) * pc) + (pfc_value_residual_unique_firstproduct))) /\ ((exists pfc_terms_code_residual_unique_firstproductcoefficient pfc_terms_scale_residual_unique_firstproductcoefficient pfc_natural_sum_residual_unique_firstproductcoefficient. ((forall pfc_index_residual_unique_firstproductcoefficientdiagonal. (exists pfa_gap_residual_unique_firstproductcoefficientdiagonalbound. pfa_gap_residual_unique_firstproductcoefficientdiagonalbound + S (pfc_index_residual_unique_firstproductcoefficientdiagonal) = (S (pfc_index_residual_unique_firstproduct))) -> exists pfc_value_residual_unique_firstproductcoefficientdiagonal. ((((exists ff_h_pfp_residual_unique_firstproductcoefficientdiagonalentry. ff_h_pfp_residual_unique_firstproductcoefficientdiagonalentry + S (pfc_value_residual_unique_firstproductcoefficientdiagonal) = S ((S (pfc_index_residual_unique_firstproductcoefficientdiagonal)) * pfc_terms_scale_residual_unique_firstproductcoefficient)) /\ exists ff_q_pfp_residual_unique_firstproductcoefficientdiagonalentry. pfc_terms_code_residual_unique_firstproductcoefficient = ff_q_pfp_residual_unique_firstproductcoefficientdiagonalentry * S ((S (pfc_index_residual_unique_firstproductcoefficientdiagonal)) * pfc_terms_scale_residual_unique_firstproductcoefficient) + (pfc_value_residual_unique_firstproductcoefficientdiagonal))) /\ ((exists pfc_complement_residual_unique_firstproductcoefficientdiagonalterm pfc_left_residual_unique_firstproductcoefficientdiagonalterm pfc_right_residual_unique_firstproductcoefficientdiagonalterm. (((pfc_index_residual_unique_firstproductcoefficientdiagonal)+pfc_complement_residual_unique_firstproductcoefficientdiagonalterm=(pfc_index_residual_unique_firstproduct)) /\ ((((((exists pfa_gap_residual_unique_firstproductcoefficientdiagonaltermleftinside. pfa_gap_residual_unique_firstproductcoefficientdiagonaltermleftinside + S (pfc_index_residual_unique_firstproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_residual_unique_firstproductcoefficientdiagonaltermleftentry. ff_h_pfp_residual_unique_firstproductcoefficientdiagonaltermleftentry + S (pfc_left_residual_unique_firstproductcoefficientdiagonalterm) = S ((S (pfc_index_residual_unique_firstproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_residual_unique_firstproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_residual_unique_firstproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_residual_unique_firstproductcoefficientdiagonal)) * qc) + (pfc_left_residual_unique_firstproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_residual_unique_firstproductcoefficientdiagonaltermleftoutside. pfc_gap_residual_unique_firstproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_residual_unique_firstproductcoefficientdiagonal)) /\ (((pfc_left_residual_unique_firstproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_residual_unique_firstproductcoefficientdiagonaltermrightinside. pfa_gap_residual_unique_firstproductcoefficientdiagonaltermrightinside + S (pfc_complement_residual_unique_firstproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_residual_unique_firstproductcoefficientdiagonaltermrightentry. ff_h_pfp_residual_unique_firstproductcoefficientdiagonaltermrightentry + S (pfc_right_residual_unique_firstproductcoefficientdiagonalterm) = S ((S (pfc_complement_residual_unique_firstproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_residual_unique_firstproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_residual_unique_firstproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_residual_unique_firstproductcoefficientdiagonalterm)) * bc) + (pfc_right_residual_unique_firstproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_residual_unique_firstproductcoefficientdiagonaltermrightoutside. pfc_gap_residual_unique_firstproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_residual_unique_firstproductcoefficientdiagonalterm)) /\ (((pfc_right_residual_unique_firstproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_residual_unique_firstproductcoefficientdiagonal)=pfc_left_residual_unique_firstproductcoefficientdiagonalterm*pfc_right_residual_unique_firstproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_residual_unique_firstproductcoefficientsum fs_v_pfc_residual_unique_firstproductcoefficientsum. ((((exists fs_h_pfc_residual_unique_firstproductcoefficientsum_body_start. fs_h_pfc_residual_unique_firstproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_residual_unique_firstproductcoefficientsum)) /\ exists fs_q_pfc_residual_unique_firstproductcoefficientsum_body_start. fs_u_pfc_residual_unique_firstproductcoefficientsum = fs_q_pfc_residual_unique_firstproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_residual_unique_firstproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_residual_unique_firstproductcoefficientsum_body_terminal. fs_h_pfc_residual_unique_firstproductcoefficientsum_body_terminal + S (pfc_natural_sum_residual_unique_firstproductcoefficient) = S ((S (S (pfc_index_residual_unique_firstproduct))) * fs_v_pfc_residual_unique_firstproductcoefficientsum)) /\ exists fs_q_pfc_residual_unique_firstproductcoefficientsum_body_terminal. fs_u_pfc_residual_unique_firstproductcoefficientsum = fs_q_pfc_residual_unique_firstproductcoefficientsum_body_terminal * S ((S (S (pfc_index_residual_unique_firstproduct))) * fs_v_pfc_residual_unique_firstproductcoefficientsum) + (pfc_natural_sum_residual_unique_firstproductcoefficient))) /\ forall fs_i_pfc_residual_unique_firstproductcoefficientsum_body_steps. (exists fs_lt_pfc_residual_unique_firstproductcoefficientsum_body_steps_bound. fs_lt_pfc_residual_unique_firstproductcoefficientsum_body_steps_bound + S fs_i_pfc_residual_unique_firstproductcoefficientsum_body_steps = S (pfc_index_residual_unique_firstproduct)) -> exists fs_a_pfc_residual_unique_firstproductcoefficientsum_body_steps fs_r_pfc_residual_unique_firstproductcoefficientsum_body_steps fs_s_pfc_residual_unique_firstproductcoefficientsum_body_steps. ((((exists fs_h_pfc_residual_unique_firstproductcoefficientsum_body_steps_summand. fs_h_pfc_residual_unique_firstproductcoefficientsum_body_steps_summand + S (fs_a_pfc_residual_unique_firstproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_residual_unique_firstproductcoefficientsum_body_steps)) * pfc_terms_scale_residual_unique_firstproductcoefficient)) /\ exists fs_q_pfc_residual_unique_firstproductcoefficientsum_body_steps_summand. pfc_terms_code_residual_unique_firstproductcoefficient = fs_q_pfc_residual_unique_firstproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_residual_unique_firstproductcoefficientsum_body_steps)) * pfc_terms_scale_residual_unique_firstproductcoefficient) + (fs_a_pfc_residual_unique_firstproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_residual_unique_firstproductcoefficientsum_body_steps_partial. fs_h_pfc_residual_unique_firstproductcoefficientsum_body_steps_partial + S (fs_r_pfc_residual_unique_firstproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_residual_unique_firstproductcoefficientsum_body_steps)) * fs_v_pfc_residual_unique_firstproductcoefficientsum)) /\ exists fs_q_pfc_residual_unique_firstproductcoefficientsum_body_steps_partial. fs_u_pfc_residual_unique_firstproductcoefficientsum = fs_q_pfc_residual_unique_firstproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_residual_unique_firstproductcoefficientsum_body_steps)) * fs_v_pfc_residual_unique_firstproductcoefficientsum) + (fs_r_pfc_residual_unique_firstproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_residual_unique_firstproductcoefficientsum_body_steps_successor. fs_h_pfc_residual_unique_firstproductcoefficientsum_body_steps_successor + S (fs_s_pfc_residual_unique_firstproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_residual_unique_firstproductcoefficientsum_body_steps)) * fs_v_pfc_residual_unique_firstproductcoefficientsum)) /\ exists fs_q_pfc_residual_unique_firstproductcoefficientsum_body_steps_successor. fs_u_pfc_residual_unique_firstproductcoefficientsum = fs_q_pfc_residual_unique_firstproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_residual_unique_firstproductcoefficientsum_body_steps)) * fs_v_pfc_residual_unique_firstproductcoefficientsum) + (fs_s_pfc_residual_unique_firstproductcoefficientsum_body_steps))) /\ fs_s_pfc_residual_unique_firstproductcoefficientsum_body_steps = fs_r_pfc_residual_unique_firstproductcoefficientsum_body_steps + fs_a_pfc_residual_unique_firstproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_residual_unique_firstproductcoefficientresiduebound. pfa_gap_residual_unique_firstproductcoefficientresiduebound + S (pfc_value_residual_unique_firstproduct) = (p)) /\ ((exists pfa_offset_left_residual_unique_firstproductcoefficientresiduecongruence pfa_offset_right_residual_unique_firstproductcoefficientresiduecongruence. (pfc_natural_sum_residual_unique_firstproductcoefficient) + (p) * pfa_offset_left_residual_unique_firstproductcoefficientresiduecongruence = (pfc_value_residual_unique_firstproduct) + (p) * pfa_offset_right_residual_unique_firstproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_residual_unique_firstdifference. (exists pfa_gap_residual_unique_firstdifferenceindex. pfa_gap_residual_unique_firstdifferenceindex + S (pfs_index_residual_unique_firstdifference) = (L)) -> exists pfs_left_residual_unique_firstdifference pfs_right_residual_unique_firstdifference pfs_result_residual_unique_firstdifference. ((((exists ff_h_pfp_residual_unique_firstdifferenceleft. ff_h_pfp_residual_unique_firstdifferenceleft + S (pfs_left_residual_unique_firstdifference) = S ((S (pfs_index_residual_unique_firstdifference)) * ac)) /\ exists ff_q_pfp_residual_unique_firstdifferenceleft. ab = ff_q_pfp_residual_unique_firstdifferenceleft * S ((S (pfs_index_residual_unique_firstdifference)) * ac) + (pfs_left_residual_unique_firstdifference))) /\ (((((exists ff_h_pfp_residual_unique_firstdifferenceright. ff_h_pfp_residual_unique_firstdifferenceright + S (pfs_right_residual_unique_firstdifference) = S ((S (pfs_index_residual_unique_firstdifference)) * pc)) /\ exists ff_q_pfp_residual_unique_firstdifferenceright. pb = ff_q_pfp_residual_unique_firstdifferenceright * S ((S (pfs_index_residual_unique_firstdifference)) * pc) + (pfs_right_residual_unique_firstdifference))) /\ (((((exists ff_h_pfp_residual_unique_firstdifferenceresult. ff_h_pfp_residual_unique_firstdifferenceresult + S (pfs_result_residual_unique_firstdifference) = S ((S (pfs_index_residual_unique_firstdifference)) * uc)) /\ exists ff_q_pfp_residual_unique_firstdifferenceresult. ub = ff_q_pfp_residual_unique_firstdifferenceresult * S ((S (pfs_index_residual_unique_firstdifference)) * uc) + (pfs_result_residual_unique_firstdifference))) /\ ((((exists pfa_gap_residual_unique_firstdifferenceoperationleft. pfa_gap_residual_unique_firstdifferenceoperationleft + S (pfs_right_residual_unique_firstdifference) = (p)) /\ (((exists pfa_gap_residual_unique_firstdifferenceoperationright. pfa_gap_residual_unique_firstdifferenceoperationright + S (pfs_result_residual_unique_firstdifference) = (p)) /\ ((((exists pfa_gap_residual_unique_firstdifferenceoperationresultbound. pfa_gap_residual_unique_firstdifferenceoperationresultbound + S (pfs_left_residual_unique_firstdifference) = (p)) /\ ((exists pfa_offset_left_residual_unique_firstdifferenceoperationresultcongruence pfa_offset_right_residual_unique_firstdifferenceoperationresultcongruence. ((pfs_right_residual_unique_firstdifference) + (pfs_result_residual_unique_firstdifference)) + (p) * pfa_offset_left_residual_unique_firstdifferenceoperationresultcongruence = (pfs_left_residual_unique_firstdifference) + (p) * pfa_offset_right_residual_unique_firstdifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(t)+(R)) /\ (((forall fom_index_pfp_residual_unique_firsttriminput. (exists fom_gap_pfp_residual_unique_firsttriminput_index_bound. fom_gap_pfp_residual_unique_firsttriminput_index_bound + S (fom_index_pfp_residual_unique_firsttriminput) = L) -> exists fom_value_pfp_residual_unique_firsttriminput. ((((exists fom_beta_height_pfp_residual_unique_firsttriminput_entry. fom_beta_height_pfp_residual_unique_firsttriminput_entry + S (fom_value_pfp_residual_unique_firsttriminput) = S ((S (fom_index_pfp_residual_unique_firsttriminput)) * uc)) /\ exists fom_beta_quotient_pfp_residual_unique_firsttriminput_entry. ub = fom_beta_quotient_pfp_residual_unique_firsttriminput_entry * S ((S (fom_index_pfp_residual_unique_firsttriminput)) * uc) + (fom_value_pfp_residual_unique_firsttriminput))) /\ (exists fom_gap_pfp_residual_unique_firsttriminput_value_bound. fom_gap_pfp_residual_unique_firsttriminput_value_bound + S (fom_value_pfp_residual_unique_firsttriminput) = p))) /\ (((forall pfp_repeat_index_residual_unique_firsttrimremoved. (exists pfa_gap_residual_unique_firsttrimremovedindex. pfa_gap_residual_unique_firsttrimremovedindex + S (pfp_repeat_index_residual_unique_firsttrimremoved) = (t)) -> (((exists ff_h_pfp_residual_unique_firsttrimremovedentry. ff_h_pfp_residual_unique_firsttrimremovedentry + S (0) = S ((S (pfp_repeat_index_residual_unique_firsttrimremoved)) * uc)) /\ exists ff_q_pfp_residual_unique_firsttrimremovedentry. ub = ff_q_pfp_residual_unique_firsttrimremovedentry * S ((S (pfp_repeat_index_residual_unique_firsttrimremoved)) * uc) + (0)))) /\ (((forall pftrim_index_residual_unique_firsttrimsuffix pftrim_value_residual_unique_firsttrimsuffix. (exists pfa_gap_residual_unique_firsttrimsuffixbound. pfa_gap_residual_unique_firsttrimsuffixbound + S (pftrim_index_residual_unique_firsttrimsuffix) = (R)) -> (((exists ff_h_pfp_residual_unique_firsttrimsuffixsource. ff_h_pfp_residual_unique_firsttrimsuffixsource + S (pftrim_value_residual_unique_firsttrimsuffix) = S ((S ((t)+pftrim_index_residual_unique_firsttrimsuffix)) * uc)) /\ exists ff_q_pfp_residual_unique_firsttrimsuffixsource. ub = ff_q_pfp_residual_unique_firsttrimsuffixsource * S ((S ((t)+pftrim_index_residual_unique_firsttrimsuffix)) * uc) + (pftrim_value_residual_unique_firsttrimsuffix))) -> (((exists ff_h_pfp_residual_unique_firsttrimsuffixoutput. ff_h_pfp_residual_unique_firsttrimsuffixoutput + S (pftrim_value_residual_unique_firsttrimsuffix) = S ((S (pftrim_index_residual_unique_firsttrimsuffix)) * rc)) /\ exists ff_q_pfp_residual_unique_firsttrimsuffixoutput. rb = ff_q_pfp_residual_unique_firsttrimsuffixoutput * S ((S (pftrim_index_residual_unique_firsttrimsuffix)) * rc) + (pftrim_value_residual_unique_firsttrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_residual_unique_firsttrimnormal. ((((exists ff_h_pfp_residual_unique_firsttrimnormalentry. ff_h_pfp_residual_unique_firsttrimnormalentry + S (pftrim_leading_residual_unique_firsttrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_residual_unique_firsttrimnormalentry. rb = ff_q_pfp_residual_unique_firsttrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_residual_unique_firsttrimnormal))) /\ ((~(pftrim_leading_residual_unique_firsttrimnormal=0)))))))))))))))))))) -> (((forall pfc_index_residual_unique_secondproduct. (exists pfa_gap_residual_unique_secondproductbound. pfa_gap_residual_unique_secondproductbound + S (pfc_index_residual_unique_secondproduct) = (L)) -> exists pfc_value_residual_unique_secondproduct. ((((exists ff_h_pfp_residual_unique_secondproductentry. ff_h_pfp_residual_unique_secondproductentry + S (pfc_value_residual_unique_secondproduct) = S ((S (pfc_index_residual_unique_secondproduct)) * PC)) /\ exists ff_q_pfp_residual_unique_secondproductentry. PB = ff_q_pfp_residual_unique_secondproductentry * S ((S (pfc_index_residual_unique_secondproduct)) * PC) + (pfc_value_residual_unique_secondproduct))) /\ ((exists pfc_terms_code_residual_unique_secondproductcoefficient pfc_terms_scale_residual_unique_secondproductcoefficient pfc_natural_sum_residual_unique_secondproductcoefficient. ((forall pfc_index_residual_unique_secondproductcoefficientdiagonal. (exists pfa_gap_residual_unique_secondproductcoefficientdiagonalbound. pfa_gap_residual_unique_secondproductcoefficientdiagonalbound + S (pfc_index_residual_unique_secondproductcoefficientdiagonal) = (S (pfc_index_residual_unique_secondproduct))) -> exists pfc_value_residual_unique_secondproductcoefficientdiagonal. ((((exists ff_h_pfp_residual_unique_secondproductcoefficientdiagonalentry. ff_h_pfp_residual_unique_secondproductcoefficientdiagonalentry + S (pfc_value_residual_unique_secondproductcoefficientdiagonal) = S ((S (pfc_index_residual_unique_secondproductcoefficientdiagonal)) * pfc_terms_scale_residual_unique_secondproductcoefficient)) /\ exists ff_q_pfp_residual_unique_secondproductcoefficientdiagonalentry. pfc_terms_code_residual_unique_secondproductcoefficient = ff_q_pfp_residual_unique_secondproductcoefficientdiagonalentry * S ((S (pfc_index_residual_unique_secondproductcoefficientdiagonal)) * pfc_terms_scale_residual_unique_secondproductcoefficient) + (pfc_value_residual_unique_secondproductcoefficientdiagonal))) /\ ((exists pfc_complement_residual_unique_secondproductcoefficientdiagonalterm pfc_left_residual_unique_secondproductcoefficientdiagonalterm pfc_right_residual_unique_secondproductcoefficientdiagonalterm. (((pfc_index_residual_unique_secondproductcoefficientdiagonal)+pfc_complement_residual_unique_secondproductcoefficientdiagonalterm=(pfc_index_residual_unique_secondproduct)) /\ ((((((exists pfa_gap_residual_unique_secondproductcoefficientdiagonaltermleftinside. pfa_gap_residual_unique_secondproductcoefficientdiagonaltermleftinside + S (pfc_index_residual_unique_secondproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_residual_unique_secondproductcoefficientdiagonaltermleftentry. ff_h_pfp_residual_unique_secondproductcoefficientdiagonaltermleftentry + S (pfc_left_residual_unique_secondproductcoefficientdiagonalterm) = S ((S (pfc_index_residual_unique_secondproductcoefficientdiagonal)) * QC)) /\ exists ff_q_pfp_residual_unique_secondproductcoefficientdiagonaltermleftentry. QB = ff_q_pfp_residual_unique_secondproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_residual_unique_secondproductcoefficientdiagonal)) * QC) + (pfc_left_residual_unique_secondproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_residual_unique_secondproductcoefficientdiagonaltermleftoutside. pfc_gap_residual_unique_secondproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_residual_unique_secondproductcoefficientdiagonal)) /\ (((pfc_left_residual_unique_secondproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_residual_unique_secondproductcoefficientdiagonaltermrightinside. pfa_gap_residual_unique_secondproductcoefficientdiagonaltermrightinside + S (pfc_complement_residual_unique_secondproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_residual_unique_secondproductcoefficientdiagonaltermrightentry. ff_h_pfp_residual_unique_secondproductcoefficientdiagonaltermrightentry + S (pfc_right_residual_unique_secondproductcoefficientdiagonalterm) = S ((S (pfc_complement_residual_unique_secondproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_residual_unique_secondproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_residual_unique_secondproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_residual_unique_secondproductcoefficientdiagonalterm)) * bc) + (pfc_right_residual_unique_secondproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_residual_unique_secondproductcoefficientdiagonaltermrightoutside. pfc_gap_residual_unique_secondproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_residual_unique_secondproductcoefficientdiagonalterm)) /\ (((pfc_right_residual_unique_secondproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_residual_unique_secondproductcoefficientdiagonal)=pfc_left_residual_unique_secondproductcoefficientdiagonalterm*pfc_right_residual_unique_secondproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_residual_unique_secondproductcoefficientsum fs_v_pfc_residual_unique_secondproductcoefficientsum. ((((exists fs_h_pfc_residual_unique_secondproductcoefficientsum_body_start. fs_h_pfc_residual_unique_secondproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_residual_unique_secondproductcoefficientsum)) /\ exists fs_q_pfc_residual_unique_secondproductcoefficientsum_body_start. fs_u_pfc_residual_unique_secondproductcoefficientsum = fs_q_pfc_residual_unique_secondproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_residual_unique_secondproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_residual_unique_secondproductcoefficientsum_body_terminal. fs_h_pfc_residual_unique_secondproductcoefficientsum_body_terminal + S (pfc_natural_sum_residual_unique_secondproductcoefficient) = S ((S (S (pfc_index_residual_unique_secondproduct))) * fs_v_pfc_residual_unique_secondproductcoefficientsum)) /\ exists fs_q_pfc_residual_unique_secondproductcoefficientsum_body_terminal. fs_u_pfc_residual_unique_secondproductcoefficientsum = fs_q_pfc_residual_unique_secondproductcoefficientsum_body_terminal * S ((S (S (pfc_index_residual_unique_secondproduct))) * fs_v_pfc_residual_unique_secondproductcoefficientsum) + (pfc_natural_sum_residual_unique_secondproductcoefficient))) /\ forall fs_i_pfc_residual_unique_secondproductcoefficientsum_body_steps. (exists fs_lt_pfc_residual_unique_secondproductcoefficientsum_body_steps_bound. fs_lt_pfc_residual_unique_secondproductcoefficientsum_body_steps_bound + S fs_i_pfc_residual_unique_secondproductcoefficientsum_body_steps = S (pfc_index_residual_unique_secondproduct)) -> exists fs_a_pfc_residual_unique_secondproductcoefficientsum_body_steps fs_r_pfc_residual_unique_secondproductcoefficientsum_body_steps fs_s_pfc_residual_unique_secondproductcoefficientsum_body_steps. ((((exists fs_h_pfc_residual_unique_secondproductcoefficientsum_body_steps_summand. fs_h_pfc_residual_unique_secondproductcoefficientsum_body_steps_summand + S (fs_a_pfc_residual_unique_secondproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_residual_unique_secondproductcoefficientsum_body_steps)) * pfc_terms_scale_residual_unique_secondproductcoefficient)) /\ exists fs_q_pfc_residual_unique_secondproductcoefficientsum_body_steps_summand. pfc_terms_code_residual_unique_secondproductcoefficient = fs_q_pfc_residual_unique_secondproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_residual_unique_secondproductcoefficientsum_body_steps)) * pfc_terms_scale_residual_unique_secondproductcoefficient) + (fs_a_pfc_residual_unique_secondproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_residual_unique_secondproductcoefficientsum_body_steps_partial. fs_h_pfc_residual_unique_secondproductcoefficientsum_body_steps_partial + S (fs_r_pfc_residual_unique_secondproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_residual_unique_secondproductcoefficientsum_body_steps)) * fs_v_pfc_residual_unique_secondproductcoefficientsum)) /\ exists fs_q_pfc_residual_unique_secondproductcoefficientsum_body_steps_partial. fs_u_pfc_residual_unique_secondproductcoefficientsum = fs_q_pfc_residual_unique_secondproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_residual_unique_secondproductcoefficientsum_body_steps)) * fs_v_pfc_residual_unique_secondproductcoefficientsum) + (fs_r_pfc_residual_unique_secondproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_residual_unique_secondproductcoefficientsum_body_steps_successor. fs_h_pfc_residual_unique_secondproductcoefficientsum_body_steps_successor + S (fs_s_pfc_residual_unique_secondproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_residual_unique_secondproductcoefficientsum_body_steps)) * fs_v_pfc_residual_unique_secondproductcoefficientsum)) /\ exists fs_q_pfc_residual_unique_secondproductcoefficientsum_body_steps_successor. fs_u_pfc_residual_unique_secondproductcoefficientsum = fs_q_pfc_residual_unique_secondproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_residual_unique_secondproductcoefficientsum_body_steps)) * fs_v_pfc_residual_unique_secondproductcoefficientsum) + (fs_s_pfc_residual_unique_secondproductcoefficientsum_body_steps))) /\ fs_s_pfc_residual_unique_secondproductcoefficientsum_body_steps = fs_r_pfc_residual_unique_secondproductcoefficientsum_body_steps + fs_a_pfc_residual_unique_secondproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_residual_unique_secondproductcoefficientresiduebound. pfa_gap_residual_unique_secondproductcoefficientresiduebound + S (pfc_value_residual_unique_secondproduct) = (p)) /\ ((exists pfa_offset_left_residual_unique_secondproductcoefficientresiduecongruence pfa_offset_right_residual_unique_secondproductcoefficientresiduecongruence. (pfc_natural_sum_residual_unique_secondproductcoefficient) + (p) * pfa_offset_left_residual_unique_secondproductcoefficientresiduecongruence = (pfc_value_residual_unique_secondproduct) + (p) * pfa_offset_right_residual_unique_secondproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_residual_unique_seconddifference. (exists pfa_gap_residual_unique_seconddifferenceindex. pfa_gap_residual_unique_seconddifferenceindex + S (pfs_index_residual_unique_seconddifference) = (L)) -> exists pfs_left_residual_unique_seconddifference pfs_right_residual_unique_seconddifference pfs_result_residual_unique_seconddifference. ((((exists ff_h_pfp_residual_unique_seconddifferenceleft. ff_h_pfp_residual_unique_seconddifferenceleft + S (pfs_left_residual_unique_seconddifference) = S ((S (pfs_index_residual_unique_seconddifference)) * ac)) /\ exists ff_q_pfp_residual_unique_seconddifferenceleft. ab = ff_q_pfp_residual_unique_seconddifferenceleft * S ((S (pfs_index_residual_unique_seconddifference)) * ac) + (pfs_left_residual_unique_seconddifference))) /\ (((((exists ff_h_pfp_residual_unique_seconddifferenceright. ff_h_pfp_residual_unique_seconddifferenceright + S (pfs_right_residual_unique_seconddifference) = S ((S (pfs_index_residual_unique_seconddifference)) * PC)) /\ exists ff_q_pfp_residual_unique_seconddifferenceright. PB = ff_q_pfp_residual_unique_seconddifferenceright * S ((S (pfs_index_residual_unique_seconddifference)) * PC) + (pfs_right_residual_unique_seconddifference))) /\ (((((exists ff_h_pfp_residual_unique_seconddifferenceresult. ff_h_pfp_residual_unique_seconddifferenceresult + S (pfs_result_residual_unique_seconddifference) = S ((S (pfs_index_residual_unique_seconddifference)) * UC)) /\ exists ff_q_pfp_residual_unique_seconddifferenceresult. UB = ff_q_pfp_residual_unique_seconddifferenceresult * S ((S (pfs_index_residual_unique_seconddifference)) * UC) + (pfs_result_residual_unique_seconddifference))) /\ ((((exists pfa_gap_residual_unique_seconddifferenceoperationleft. pfa_gap_residual_unique_seconddifferenceoperationleft + S (pfs_right_residual_unique_seconddifference) = (p)) /\ (((exists pfa_gap_residual_unique_seconddifferenceoperationright. pfa_gap_residual_unique_seconddifferenceoperationright + S (pfs_result_residual_unique_seconddifference) = (p)) /\ ((((exists pfa_gap_residual_unique_seconddifferenceoperationresultbound. pfa_gap_residual_unique_seconddifferenceoperationresultbound + S (pfs_left_residual_unique_seconddifference) = (p)) /\ ((exists pfa_offset_left_residual_unique_seconddifferenceoperationresultcongruence pfa_offset_right_residual_unique_seconddifferenceoperationresultcongruence. ((pfs_right_residual_unique_seconddifference) + (pfs_result_residual_unique_seconddifference)) + (p) * pfa_offset_left_residual_unique_seconddifferenceoperationresultcongruence = (pfs_left_residual_unique_seconddifference) + (p) * pfa_offset_right_residual_unique_seconddifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(T)+(K)) /\ (((forall fom_index_pfp_residual_unique_secondtriminput. (exists fom_gap_pfp_residual_unique_secondtriminput_index_bound. fom_gap_pfp_residual_unique_secondtriminput_index_bound + S (fom_index_pfp_residual_unique_secondtriminput) = L) -> exists fom_value_pfp_residual_unique_secondtriminput. ((((exists fom_beta_height_pfp_residual_unique_secondtriminput_entry. fom_beta_height_pfp_residual_unique_secondtriminput_entry + S (fom_value_pfp_residual_unique_secondtriminput) = S ((S (fom_index_pfp_residual_unique_secondtriminput)) * UC)) /\ exists fom_beta_quotient_pfp_residual_unique_secondtriminput_entry. UB = fom_beta_quotient_pfp_residual_unique_secondtriminput_entry * S ((S (fom_index_pfp_residual_unique_secondtriminput)) * UC) + (fom_value_pfp_residual_unique_secondtriminput))) /\ (exists fom_gap_pfp_residual_unique_secondtriminput_value_bound. fom_gap_pfp_residual_unique_secondtriminput_value_bound + S (fom_value_pfp_residual_unique_secondtriminput) = p))) /\ (((forall pfp_repeat_index_residual_unique_secondtrimremoved. (exists pfa_gap_residual_unique_secondtrimremovedindex. pfa_gap_residual_unique_secondtrimremovedindex + S (pfp_repeat_index_residual_unique_secondtrimremoved) = (T)) -> (((exists ff_h_pfp_residual_unique_secondtrimremovedentry. ff_h_pfp_residual_unique_secondtrimremovedentry + S (0) = S ((S (pfp_repeat_index_residual_unique_secondtrimremoved)) * UC)) /\ exists ff_q_pfp_residual_unique_secondtrimremovedentry. UB = ff_q_pfp_residual_unique_secondtrimremovedentry * S ((S (pfp_repeat_index_residual_unique_secondtrimremoved)) * UC) + (0)))) /\ (((forall pftrim_index_residual_unique_secondtrimsuffix pftrim_value_residual_unique_secondtrimsuffix. (exists pfa_gap_residual_unique_secondtrimsuffixbound. pfa_gap_residual_unique_secondtrimsuffixbound + S (pftrim_index_residual_unique_secondtrimsuffix) = (K)) -> (((exists ff_h_pfp_residual_unique_secondtrimsuffixsource. ff_h_pfp_residual_unique_secondtrimsuffixsource + S (pftrim_value_residual_unique_secondtrimsuffix) = S ((S ((T)+pftrim_index_residual_unique_secondtrimsuffix)) * UC)) /\ exists ff_q_pfp_residual_unique_secondtrimsuffixsource. UB = ff_q_pfp_residual_unique_secondtrimsuffixsource * S ((S ((T)+pftrim_index_residual_unique_secondtrimsuffix)) * UC) + (pftrim_value_residual_unique_secondtrimsuffix))) -> (((exists ff_h_pfp_residual_unique_secondtrimsuffixoutput. ff_h_pfp_residual_unique_secondtrimsuffixoutput + S (pftrim_value_residual_unique_secondtrimsuffix) = S ((S (pftrim_index_residual_unique_secondtrimsuffix)) * RC)) /\ exists ff_q_pfp_residual_unique_secondtrimsuffixoutput. RB = ff_q_pfp_residual_unique_secondtrimsuffixoutput * S ((S (pftrim_index_residual_unique_secondtrimsuffix)) * RC) + (pftrim_value_residual_unique_secondtrimsuffix)))) /\ (((K)=0 \/ (exists pftrim_leading_residual_unique_secondtrimnormal. ((((exists ff_h_pfp_residual_unique_secondtrimnormalentry. ff_h_pfp_residual_unique_secondtrimnormalentry + S (pftrim_leading_residual_unique_secondtrimnormal) = S ((S (0)) * RC)) /\ exists ff_q_pfp_residual_unique_secondtrimnormalentry. RB = ff_q_pfp_residual_unique_secondtrimnormalentry * S ((S (0)) * RC) + (pftrim_leading_residual_unique_secondtrimnormal))) /\ ((~(pftrim_leading_residual_unique_secondtrimnormal=0)))))))))))))))))))) -> (((t=T) /\ (((R=K) /\ ((forall mdr_i_pfp_residual_unique_output mdr_a_pfp_residual_unique_output. (exists mdr_gap_pfp_residual_unique_outputb. mdr_gap_pfp_residual_unique_outputb + S (mdr_i_pfp_residual_unique_output) = (R)) -> (((exists ff_h_mdr_pfp_residual_unique_outputo. ff_h_mdr_pfp_residual_unique_outputo + S (mdr_a_pfp_residual_unique_output) = S ((S (mdr_i_pfp_residual_unique_output)) * rc)) /\ exists ff_q_mdr_pfp_residual_unique_outputo. rb = ff_q_mdr_pfp_residual_unique_outputo * S ((S (mdr_i_pfp_residual_unique_output)) * rc) + (mdr_a_pfp_residual_unique_output))) -> (((exists ff_h_mdr_pfp_residual_unique_outputn. ff_h_mdr_pfp_residual_unique_outputn + S (mdr_a_pfp_residual_unique_output) = S ((S (mdr_i_pfp_residual_unique_output)) * RC)) /\ exists ff_q_mdr_pfp_residual_unique_outputn. RB = ff_q_mdr_pfp_residual_unique_outputn * S ((S (mdr_i_pfp_residual_unique_output)) * RC) + (mdr_a_pfp_residual_unique_output)))))))))