prime_field_polynomial_division_remainder_length_descent

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc d qb qc q rb rc R. (~((p) = 1) /\ forall pfa_factor_left_normalization_descent_prime pfa_factor_right_normalization_descent_prime. (p) = pfa_factor_left_normalization_descent_prime * pfa_factor_right_normalization_descent_prime -> pfa_factor_left_normalization_descent_prime = 1 \/ pfa_factor_right_normalization_descent_prime = 1) -> (((forall fom_index_pfp_normalization_descent_executioninput. (exists fom_gap_pfp_normalization_descent_executioninput_index_bound. fom_gap_pfp_normalization_descent_executioninput_index_bound + S (fom_index_pfp_normalization_descent_executioninput) = L) -> exists fom_value_pfp_normalization_descent_executioninput. ((((exists fom_beta_height_pfp_normalization_descent_executioninput_entry. fom_beta_height_pfp_normalization_descent_executioninput_entry + S (fom_value_pfp_normalization_descent_executioninput) = S ((S (fom_index_pfp_normalization_descent_executioninput)) * ac)) /\ exists fom_beta_quotient_pfp_normalization_descent_executioninput_entry. ab = fom_beta_quotient_pfp_normalization_descent_executioninput_entry * S ((S (fom_index_pfp_normalization_descent_executioninput)) * ac) + (fom_value_pfp_normalization_descent_executioninput))) /\ (exists fom_gap_pfp_normalization_descent_executioninput_value_bound. fom_gap_pfp_normalization_descent_executioninput_value_bound + S (fom_value_pfp_normalization_descent_executioninput) = p))) /\ (((forall fom_index_pfp_normalization_descent_executiondivisor. (exists fom_gap_pfp_normalization_descent_executiondivisor_index_bound. fom_gap_pfp_normalization_descent_executiondivisor_index_bound + S (fom_index_pfp_normalization_descent_executiondivisor) = S (d)) -> exists fom_value_pfp_normalization_descent_executiondivisor. ((((exists fom_beta_height_pfp_normalization_descent_executiondivisor_entry. fom_beta_height_pfp_normalization_descent_executiondivisor_entry + S (fom_value_pfp_normalization_descent_executiondivisor) = S ((S (fom_index_pfp_normalization_descent_executiondivisor)) * bc)) /\ exists fom_beta_quotient_pfp_normalization_descent_executiondivisor_entry. bb = fom_beta_quotient_pfp_normalization_descent_executiondivisor_entry * S ((S (fom_index_pfp_normalization_descent_executiondivisor)) * bc) + (fom_value_pfp_normalization_descent_executiondivisor))) /\ (exists fom_gap_pfp_normalization_descent_executiondivisor_value_bound. fom_gap_pfp_normalization_descent_executiondivisor_value_bound + S (fom_value_pfp_normalization_descent_executiondivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_normalization_descent_executionlengthshort. pfc_gap_normalization_descent_executionlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_normalization_descent_execution pfd_inverse_normalization_descent_execution pfd_product_code_normalization_descent_execution pfd_product_scale_normalization_descent_execution pfd_residual_code_normalization_descent_execution pfd_residual_scale_normalization_descent_execution pfd_cut_normalization_descent_execution. ((((exists ff_h_pfp_normalization_descent_executionhead. ff_h_pfp_normalization_descent_executionhead + S (pfd_head_normalization_descent_execution) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_descent_executionhead. bb = ff_q_pfp_normalization_descent_executionhead * S ((S (0)) * bc) + (pfd_head_normalization_descent_execution))) /\ (((((~((pfd_head_normalization_descent_execution) = 0)) /\ ((((exists pfa_gap_normalization_descent_executioninversemultiplicationleft. pfa_gap_normalization_descent_executioninversemultiplicationleft + S (pfd_head_normalization_descent_execution) = (p)) /\ (((exists pfa_gap_normalization_descent_executioninversemultiplicationright. pfa_gap_normalization_descent_executioninversemultiplicationright + S (pfd_inverse_normalization_descent_execution) = (p)) /\ ((((exists pfa_gap_normalization_descent_executioninversemultiplicationresultbound. pfa_gap_normalization_descent_executioninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_descent_executioninversemultiplicationresultcongruence pfa_offset_right_normalization_descent_executioninversemultiplicationresultcongruence. ((pfd_head_normalization_descent_execution) * (pfd_inverse_normalization_descent_execution)) + (p) * pfa_offset_left_normalization_descent_executioninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_descent_executioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_normalization_descent_executionquotient. (exists pfa_gap_normalization_descent_executionquotientbound. pfa_gap_normalization_descent_executionquotientbound + S (pfd_index_normalization_descent_executionquotient) = (q)) -> exists pfd_value_normalization_descent_executionquotient. ((((exists ff_h_pfp_normalization_descent_executionquotiententry. ff_h_pfp_normalization_descent_executionquotiententry + S (pfd_value_normalization_descent_executionquotient) = S ((S (pfd_index_normalization_descent_executionquotient)) * qc)) /\ exists ff_q_pfp_normalization_descent_executionquotiententry. qb = ff_q_pfp_normalization_descent_executionquotiententry * S ((S (pfd_index_normalization_descent_executionquotient)) * qc) + (pfd_value_normalization_descent_executionquotient))) /\ ((exists pfd_input_normalization_descent_executionquotientstep pfd_previous_normalization_descent_executionquotientstep pfd_difference_normalization_descent_executionquotientstep. ((((exists ff_h_pfp_normalization_descent_executionquotientstepinput. ff_h_pfp_normalization_descent_executionquotientstepinput + S (pfd_input_normalization_descent_executionquotientstep) = S ((S (pfd_index_normalization_descent_executionquotient)) * ac)) /\ exists ff_q_pfp_normalization_descent_executionquotientstepinput. ab = ff_q_pfp_normalization_descent_executionquotientstepinput * S ((S (pfd_index_normalization_descent_executionquotient)) * ac) + (pfd_input_normalization_descent_executionquotientstep))) /\ (((exists pfc_terms_code_normalization_descent_executionquotientstepprevious pfc_terms_scale_normalization_descent_executionquotientstepprevious pfc_natural_sum_normalization_descent_executionquotientstepprevious. ((forall pfc_index_normalization_descent_executionquotientsteppreviousdiagonal. (exists pfa_gap_normalization_descent_executionquotientsteppreviousdiagonalbound. pfa_gap_normalization_descent_executionquotientsteppreviousdiagonalbound + S (pfc_index_normalization_descent_executionquotientsteppreviousdiagonal) = (S (pfd_index_normalization_descent_executionquotient))) -> exists pfc_value_normalization_descent_executionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_normalization_descent_executionquotientsteppreviousdiagonalentry. ff_h_pfp_normalization_descent_executionquotientsteppreviousdiagonalentry + S (pfc_value_normalization_descent_executionquotientsteppreviousdiagonal) = S ((S (pfc_index_normalization_descent_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_normalization_descent_executionquotientstepprevious)) /\ exists ff_q_pfp_normalization_descent_executionquotientsteppreviousdiagonalentry. pfc_terms_code_normalization_descent_executionquotientstepprevious = ff_q_pfp_normalization_descent_executionquotientsteppreviousdiagonalentry * S ((S (pfc_index_normalization_descent_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_normalization_descent_executionquotientstepprevious) + (pfc_value_normalization_descent_executionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_normalization_descent_executionquotientsteppreviousdiagonalterm pfc_left_normalization_descent_executionquotientsteppreviousdiagonalterm pfc_right_normalization_descent_executionquotientsteppreviousdiagonalterm. (((pfc_index_normalization_descent_executionquotientsteppreviousdiagonal)+pfc_complement_normalization_descent_executionquotientsteppreviousdiagonalterm=(pfd_index_normalization_descent_executionquotient)) /\ ((((((exists pfa_gap_normalization_descent_executionquotientsteppreviousdiagonaltermleftinside. pfa_gap_normalization_descent_executionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_normalization_descent_executionquotientsteppreviousdiagonal) = (pfd_index_normalization_descent_executionquotient)) /\ ((((exists ff_h_pfp_normalization_descent_executionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_normalization_descent_executionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_normalization_descent_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_normalization_descent_executionquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_normalization_descent_executionquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_normalization_descent_executionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_normalization_descent_executionquotientsteppreviousdiagonal)) * qc) + (pfc_left_normalization_descent_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_normalization_descent_executionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_normalization_descent_executionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_normalization_descent_executionquotient)=(pfc_index_normalization_descent_executionquotientsteppreviousdiagonal)) /\ (((pfc_left_normalization_descent_executionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalization_descent_executionquotientsteppreviousdiagonaltermrightinside. pfa_gap_normalization_descent_executionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_normalization_descent_executionquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_normalization_descent_executionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_normalization_descent_executionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_normalization_descent_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_normalization_descent_executionquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_normalization_descent_executionquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_normalization_descent_executionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_normalization_descent_executionquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_normalization_descent_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_normalization_descent_executionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_normalization_descent_executionquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_normalization_descent_executionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_normalization_descent_executionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_normalization_descent_executionquotientsteppreviousdiagonal)=pfc_left_normalization_descent_executionquotientsteppreviousdiagonalterm*pfc_right_normalization_descent_executionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalization_descent_executionquotientstepprevioussum fs_v_pfc_normalization_descent_executionquotientstepprevioussum. ((((exists fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_start. fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalization_descent_executionquotientstepprevioussum)) /\ exists fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_start. fs_u_pfc_normalization_descent_executionquotientstepprevioussum = fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_normalization_descent_executionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_terminal. fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_normalization_descent_executionquotientstepprevious) = S ((S (S (pfd_index_normalization_descent_executionquotient))) * fs_v_pfc_normalization_descent_executionquotientstepprevioussum)) /\ exists fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_terminal. fs_u_pfc_normalization_descent_executionquotientstepprevioussum = fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_normalization_descent_executionquotient))) * fs_v_pfc_normalization_descent_executionquotientstepprevioussum) + (pfc_natural_sum_normalization_descent_executionquotientstepprevious))) /\ forall fs_i_pfc_normalization_descent_executionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_normalization_descent_executionquotientstepprevioussum_body_steps = S (pfd_index_normalization_descent_executionquotient)) -> exists fs_a_pfc_normalization_descent_executionquotientstepprevioussum_body_steps fs_r_pfc_normalization_descent_executionquotientstepprevioussum_body_steps fs_s_pfc_normalization_descent_executionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_summand. fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_normalization_descent_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_normalization_descent_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_normalization_descent_executionquotientstepprevious)) /\ exists fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_summand. pfc_terms_code_normalization_descent_executionquotientstepprevious = fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_normalization_descent_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_normalization_descent_executionquotientstepprevious) + (fs_a_pfc_normalization_descent_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_partial. fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_normalization_descent_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_normalization_descent_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_normalization_descent_executionquotientstepprevioussum)) /\ exists fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_partial. fs_u_pfc_normalization_descent_executionquotientstepprevioussum = fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_normalization_descent_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_normalization_descent_executionquotientstepprevioussum) + (fs_r_pfc_normalization_descent_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_successor. fs_h_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_normalization_descent_executionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_normalization_descent_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_normalization_descent_executionquotientstepprevioussum)) /\ exists fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_successor. fs_u_pfc_normalization_descent_executionquotientstepprevioussum = fs_q_pfc_normalization_descent_executionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_normalization_descent_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_normalization_descent_executionquotientstepprevioussum) + (fs_s_pfc_normalization_descent_executionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_normalization_descent_executionquotientstepprevioussum_body_steps = fs_r_pfc_normalization_descent_executionquotientstepprevioussum_body_steps + fs_a_pfc_normalization_descent_executionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_normalization_descent_executionquotientsteppreviousresiduebound. pfa_gap_normalization_descent_executionquotientsteppreviousresiduebound + S (pfd_previous_normalization_descent_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_normalization_descent_executionquotientsteppreviousresiduecongruence pfa_offset_right_normalization_descent_executionquotientsteppreviousresiduecongruence. (pfc_natural_sum_normalization_descent_executionquotientstepprevious) + (p) * pfa_offset_left_normalization_descent_executionquotientsteppreviousresiduecongruence = (pfd_previous_normalization_descent_executionquotientstep) + (p) * pfa_offset_right_normalization_descent_executionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_normalization_descent_executionquotientstepsubtractleft. pfa_gap_normalization_descent_executionquotientstepsubtractleft + S (pfd_previous_normalization_descent_executionquotientstep) = (p)) /\ (((exists pfa_gap_normalization_descent_executionquotientstepsubtractright. pfa_gap_normalization_descent_executionquotientstepsubtractright + S (pfd_difference_normalization_descent_executionquotientstep) = (p)) /\ ((((exists pfa_gap_normalization_descent_executionquotientstepsubtractresultbound. pfa_gap_normalization_descent_executionquotientstepsubtractresultbound + S (pfd_input_normalization_descent_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_normalization_descent_executionquotientstepsubtractresultcongruence pfa_offset_right_normalization_descent_executionquotientstepsubtractresultcongruence. ((pfd_previous_normalization_descent_executionquotientstep) + (pfd_difference_normalization_descent_executionquotientstep)) + (p) * pfa_offset_left_normalization_descent_executionquotientstepsubtractresultcongruence = (pfd_input_normalization_descent_executionquotientstep) + (p) * pfa_offset_right_normalization_descent_executionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_normalization_descent_executionquotientstepmultiplyleft. pfa_gap_normalization_descent_executionquotientstepmultiplyleft + S (pfd_inverse_normalization_descent_execution) = (p)) /\ (((exists pfa_gap_normalization_descent_executionquotientstepmultiplyright. pfa_gap_normalization_descent_executionquotientstepmultiplyright + S (pfd_difference_normalization_descent_executionquotientstep) = (p)) /\ ((((exists pfa_gap_normalization_descent_executionquotientstepmultiplyresultbound. pfa_gap_normalization_descent_executionquotientstepmultiplyresultbound + S (pfd_value_normalization_descent_executionquotient) = (p)) /\ ((exists pfa_offset_left_normalization_descent_executionquotientstepmultiplyresultcongruence pfa_offset_right_normalization_descent_executionquotientstepmultiplyresultcongruence. ((pfd_inverse_normalization_descent_execution) * (pfd_difference_normalization_descent_executionquotientstep)) + (p) * pfa_offset_left_normalization_descent_executionquotientstepmultiplyresultcongruence = (pfd_value_normalization_descent_executionquotient) + (p) * pfa_offset_right_normalization_descent_executionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_normalization_descent_executionproduct. (exists pfa_gap_normalization_descent_executionproductbound. pfa_gap_normalization_descent_executionproductbound + S (pfc_index_normalization_descent_executionproduct) = (L)) -> exists pfc_value_normalization_descent_executionproduct. ((((exists ff_h_pfp_normalization_descent_executionproductentry. ff_h_pfp_normalization_descent_executionproductentry + S (pfc_value_normalization_descent_executionproduct) = S ((S (pfc_index_normalization_descent_executionproduct)) * pfd_product_scale_normalization_descent_execution)) /\ exists ff_q_pfp_normalization_descent_executionproductentry. pfd_product_code_normalization_descent_execution = ff_q_pfp_normalization_descent_executionproductentry * S ((S (pfc_index_normalization_descent_executionproduct)) * pfd_product_scale_normalization_descent_execution) + (pfc_value_normalization_descent_executionproduct))) /\ ((exists pfc_terms_code_normalization_descent_executionproductcoefficient pfc_terms_scale_normalization_descent_executionproductcoefficient pfc_natural_sum_normalization_descent_executionproductcoefficient. ((forall pfc_index_normalization_descent_executionproductcoefficientdiagonal. (exists pfa_gap_normalization_descent_executionproductcoefficientdiagonalbound. pfa_gap_normalization_descent_executionproductcoefficientdiagonalbound + S (pfc_index_normalization_descent_executionproductcoefficientdiagonal) = (S (pfc_index_normalization_descent_executionproduct))) -> exists pfc_value_normalization_descent_executionproductcoefficientdiagonal. ((((exists ff_h_pfp_normalization_descent_executionproductcoefficientdiagonalentry. ff_h_pfp_normalization_descent_executionproductcoefficientdiagonalentry + S (pfc_value_normalization_descent_executionproductcoefficientdiagonal) = S ((S (pfc_index_normalization_descent_executionproductcoefficientdiagonal)) * pfc_terms_scale_normalization_descent_executionproductcoefficient)) /\ exists ff_q_pfp_normalization_descent_executionproductcoefficientdiagonalentry. pfc_terms_code_normalization_descent_executionproductcoefficient = ff_q_pfp_normalization_descent_executionproductcoefficientdiagonalentry * S ((S (pfc_index_normalization_descent_executionproductcoefficientdiagonal)) * pfc_terms_scale_normalization_descent_executionproductcoefficient) + (pfc_value_normalization_descent_executionproductcoefficientdiagonal))) /\ ((exists pfc_complement_normalization_descent_executionproductcoefficientdiagonalterm pfc_left_normalization_descent_executionproductcoefficientdiagonalterm pfc_right_normalization_descent_executionproductcoefficientdiagonalterm. (((pfc_index_normalization_descent_executionproductcoefficientdiagonal)+pfc_complement_normalization_descent_executionproductcoefficientdiagonalterm=(pfc_index_normalization_descent_executionproduct)) /\ ((((((exists pfa_gap_normalization_descent_executionproductcoefficientdiagonaltermleftinside. pfa_gap_normalization_descent_executionproductcoefficientdiagonaltermleftinside + S (pfc_index_normalization_descent_executionproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_normalization_descent_executionproductcoefficientdiagonaltermleftentry. ff_h_pfp_normalization_descent_executionproductcoefficientdiagonaltermleftentry + S (pfc_left_normalization_descent_executionproductcoefficientdiagonalterm) = S ((S (pfc_index_normalization_descent_executionproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_normalization_descent_executionproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_normalization_descent_executionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_normalization_descent_executionproductcoefficientdiagonal)) * qc) + (pfc_left_normalization_descent_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_descent_executionproductcoefficientdiagonaltermleftoutside. pfc_gap_normalization_descent_executionproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_normalization_descent_executionproductcoefficientdiagonal)) /\ (((pfc_left_normalization_descent_executionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalization_descent_executionproductcoefficientdiagonaltermrightinside. pfa_gap_normalization_descent_executionproductcoefficientdiagonaltermrightinside + S (pfc_complement_normalization_descent_executionproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_normalization_descent_executionproductcoefficientdiagonaltermrightentry. ff_h_pfp_normalization_descent_executionproductcoefficientdiagonaltermrightentry + S (pfc_right_normalization_descent_executionproductcoefficientdiagonalterm) = S ((S (pfc_complement_normalization_descent_executionproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_normalization_descent_executionproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_normalization_descent_executionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalization_descent_executionproductcoefficientdiagonalterm)) * bc) + (pfc_right_normalization_descent_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_descent_executionproductcoefficientdiagonaltermrightoutside. pfc_gap_normalization_descent_executionproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_normalization_descent_executionproductcoefficientdiagonalterm)) /\ (((pfc_right_normalization_descent_executionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalization_descent_executionproductcoefficientdiagonal)=pfc_left_normalization_descent_executionproductcoefficientdiagonalterm*pfc_right_normalization_descent_executionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalization_descent_executionproductcoefficientsum fs_v_pfc_normalization_descent_executionproductcoefficientsum. ((((exists fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_start. fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalization_descent_executionproductcoefficientsum)) /\ exists fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_start. fs_u_pfc_normalization_descent_executionproductcoefficientsum = fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalization_descent_executionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_terminal. fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_terminal + S (pfc_natural_sum_normalization_descent_executionproductcoefficient) = S ((S (S (pfc_index_normalization_descent_executionproduct))) * fs_v_pfc_normalization_descent_executionproductcoefficientsum)) /\ exists fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_terminal. fs_u_pfc_normalization_descent_executionproductcoefficientsum = fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_normalization_descent_executionproduct))) * fs_v_pfc_normalization_descent_executionproductcoefficientsum) + (pfc_natural_sum_normalization_descent_executionproductcoefficient))) /\ forall fs_i_pfc_normalization_descent_executionproductcoefficientsum_body_steps. (exists fs_lt_pfc_normalization_descent_executionproductcoefficientsum_body_steps_bound. fs_lt_pfc_normalization_descent_executionproductcoefficientsum_body_steps_bound + S fs_i_pfc_normalization_descent_executionproductcoefficientsum_body_steps = S (pfc_index_normalization_descent_executionproduct)) -> exists fs_a_pfc_normalization_descent_executionproductcoefficientsum_body_steps fs_r_pfc_normalization_descent_executionproductcoefficientsum_body_steps fs_s_pfc_normalization_descent_executionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_steps_summand. fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_normalization_descent_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_descent_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_normalization_descent_executionproductcoefficient)) /\ exists fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_steps_summand. pfc_terms_code_normalization_descent_executionproductcoefficient = fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalization_descent_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_normalization_descent_executionproductcoefficient) + (fs_a_pfc_normalization_descent_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_steps_partial. fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_normalization_descent_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_descent_executionproductcoefficientsum_body_steps)) * fs_v_pfc_normalization_descent_executionproductcoefficientsum)) /\ exists fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_steps_partial. fs_u_pfc_normalization_descent_executionproductcoefficientsum = fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalization_descent_executionproductcoefficientsum_body_steps)) * fs_v_pfc_normalization_descent_executionproductcoefficientsum) + (fs_r_pfc_normalization_descent_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_steps_successor. fs_h_pfc_normalization_descent_executionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_normalization_descent_executionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalization_descent_executionproductcoefficientsum_body_steps)) * fs_v_pfc_normalization_descent_executionproductcoefficientsum)) /\ exists fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_steps_successor. fs_u_pfc_normalization_descent_executionproductcoefficientsum = fs_q_pfc_normalization_descent_executionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalization_descent_executionproductcoefficientsum_body_steps)) * fs_v_pfc_normalization_descent_executionproductcoefficientsum) + (fs_s_pfc_normalization_descent_executionproductcoefficientsum_body_steps))) /\ fs_s_pfc_normalization_descent_executionproductcoefficientsum_body_steps = fs_r_pfc_normalization_descent_executionproductcoefficientsum_body_steps + fs_a_pfc_normalization_descent_executionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalization_descent_executionproductcoefficientresiduebound. pfa_gap_normalization_descent_executionproductcoefficientresiduebound + S (pfc_value_normalization_descent_executionproduct) = (p)) /\ ((exists pfa_offset_left_normalization_descent_executionproductcoefficientresiduecongruence pfa_offset_right_normalization_descent_executionproductcoefficientresiduecongruence. (pfc_natural_sum_normalization_descent_executionproductcoefficient) + (p) * pfa_offset_left_normalization_descent_executionproductcoefficientresiduecongruence = (pfc_value_normalization_descent_executionproduct) + (p) * pfa_offset_right_normalization_descent_executionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_normalization_descent_executiondifference. (exists pfa_gap_normalization_descent_executiondifferenceindex. pfa_gap_normalization_descent_executiondifferenceindex + S (pfs_index_normalization_descent_executiondifference) = (L)) -> exists pfs_left_normalization_descent_executiondifference pfs_right_normalization_descent_executiondifference pfs_result_normalization_descent_executiondifference. ((((exists ff_h_pfp_normalization_descent_executiondifferenceleft. ff_h_pfp_normalization_descent_executiondifferenceleft + S (pfs_left_normalization_descent_executiondifference) = S ((S (pfs_index_normalization_descent_executiondifference)) * ac)) /\ exists ff_q_pfp_normalization_descent_executiondifferenceleft. ab = ff_q_pfp_normalization_descent_executiondifferenceleft * S ((S (pfs_index_normalization_descent_executiondifference)) * ac) + (pfs_left_normalization_descent_executiondifference))) /\ (((((exists ff_h_pfp_normalization_descent_executiondifferenceright. ff_h_pfp_normalization_descent_executiondifferenceright + S (pfs_right_normalization_descent_executiondifference) = S ((S (pfs_index_normalization_descent_executiondifference)) * pfd_product_scale_normalization_descent_execution)) /\ exists ff_q_pfp_normalization_descent_executiondifferenceright. pfd_product_code_normalization_descent_execution = ff_q_pfp_normalization_descent_executiondifferenceright * S ((S (pfs_index_normalization_descent_executiondifference)) * pfd_product_scale_normalization_descent_execution) + (pfs_right_normalization_descent_executiondifference))) /\ (((((exists ff_h_pfp_normalization_descent_executiondifferenceresult. ff_h_pfp_normalization_descent_executiondifferenceresult + S (pfs_result_normalization_descent_executiondifference) = S ((S (pfs_index_normalization_descent_executiondifference)) * pfd_residual_scale_normalization_descent_execution)) /\ exists ff_q_pfp_normalization_descent_executiondifferenceresult. pfd_residual_code_normalization_descent_execution = ff_q_pfp_normalization_descent_executiondifferenceresult * S ((S (pfs_index_normalization_descent_executiondifference)) * pfd_residual_scale_normalization_descent_execution) + (pfs_result_normalization_descent_executiondifference))) /\ ((((exists pfa_gap_normalization_descent_executiondifferenceoperationleft. pfa_gap_normalization_descent_executiondifferenceoperationleft + S (pfs_right_normalization_descent_executiondifference) = (p)) /\ (((exists pfa_gap_normalization_descent_executiondifferenceoperationright. pfa_gap_normalization_descent_executiondifferenceoperationright + S (pfs_result_normalization_descent_executiondifference) = (p)) /\ ((((exists pfa_gap_normalization_descent_executiondifferenceoperationresultbound. pfa_gap_normalization_descent_executiondifferenceoperationresultbound + S (pfs_left_normalization_descent_executiondifference) = (p)) /\ ((exists pfa_offset_left_normalization_descent_executiondifferenceoperationresultcongruence pfa_offset_right_normalization_descent_executiondifferenceoperationresultcongruence. ((pfs_right_normalization_descent_executiondifference) + (pfs_result_normalization_descent_executiondifference)) + (p) * pfa_offset_left_normalization_descent_executiondifferenceoperationresultcongruence = (pfs_left_normalization_descent_executiondifference) + (p) * pfa_offset_right_normalization_descent_executiondifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_normalization_descent_execution)+(R)) /\ (((forall fom_index_pfp_normalization_descent_executiontriminput. (exists fom_gap_pfp_normalization_descent_executiontriminput_index_bound. fom_gap_pfp_normalization_descent_executiontriminput_index_bound + S (fom_index_pfp_normalization_descent_executiontriminput) = L) -> exists fom_value_pfp_normalization_descent_executiontriminput. ((((exists fom_beta_height_pfp_normalization_descent_executiontriminput_entry. fom_beta_height_pfp_normalization_descent_executiontriminput_entry + S (fom_value_pfp_normalization_descent_executiontriminput) = S ((S (fom_index_pfp_normalization_descent_executiontriminput)) * pfd_residual_scale_normalization_descent_execution)) /\ exists fom_beta_quotient_pfp_normalization_descent_executiontriminput_entry. pfd_residual_code_normalization_descent_execution = fom_beta_quotient_pfp_normalization_descent_executiontriminput_entry * S ((S (fom_index_pfp_normalization_descent_executiontriminput)) * pfd_residual_scale_normalization_descent_execution) + (fom_value_pfp_normalization_descent_executiontriminput))) /\ (exists fom_gap_pfp_normalization_descent_executiontriminput_value_bound. fom_gap_pfp_normalization_descent_executiontriminput_value_bound + S (fom_value_pfp_normalization_descent_executiontriminput) = p))) /\ (((forall pfp_repeat_index_normalization_descent_executiontrimremoved. (exists pfa_gap_normalization_descent_executiontrimremovedindex. pfa_gap_normalization_descent_executiontrimremovedindex + S (pfp_repeat_index_normalization_descent_executiontrimremoved) = (pfd_cut_normalization_descent_execution)) -> (((exists ff_h_pfp_normalization_descent_executiontrimremovedentry. ff_h_pfp_normalization_descent_executiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_normalization_descent_executiontrimremoved)) * pfd_residual_scale_normalization_descent_execution)) /\ exists ff_q_pfp_normalization_descent_executiontrimremovedentry. pfd_residual_code_normalization_descent_execution = ff_q_pfp_normalization_descent_executiontrimremovedentry * S ((S (pfp_repeat_index_normalization_descent_executiontrimremoved)) * pfd_residual_scale_normalization_descent_execution) + (0)))) /\ (((forall pftrim_index_normalization_descent_executiontrimsuffix pftrim_value_normalization_descent_executiontrimsuffix. (exists pfa_gap_normalization_descent_executiontrimsuffixbound. pfa_gap_normalization_descent_executiontrimsuffixbound + S (pftrim_index_normalization_descent_executiontrimsuffix) = (R)) -> (((exists ff_h_pfp_normalization_descent_executiontrimsuffixsource. ff_h_pfp_normalization_descent_executiontrimsuffixsource + S (pftrim_value_normalization_descent_executiontrimsuffix) = S ((S ((pfd_cut_normalization_descent_execution)+pftrim_index_normalization_descent_executiontrimsuffix)) * pfd_residual_scale_normalization_descent_execution)) /\ exists ff_q_pfp_normalization_descent_executiontrimsuffixsource. pfd_residual_code_normalization_descent_execution = ff_q_pfp_normalization_descent_executiontrimsuffixsource * S ((S ((pfd_cut_normalization_descent_execution)+pftrim_index_normalization_descent_executiontrimsuffix)) * pfd_residual_scale_normalization_descent_execution) + (pftrim_value_normalization_descent_executiontrimsuffix))) -> (((exists ff_h_pfp_normalization_descent_executiontrimsuffixoutput. ff_h_pfp_normalization_descent_executiontrimsuffixoutput + S (pftrim_value_normalization_descent_executiontrimsuffix) = S ((S (pftrim_index_normalization_descent_executiontrimsuffix)) * rc)) /\ exists ff_q_pfp_normalization_descent_executiontrimsuffixoutput. rb = ff_q_pfp_normalization_descent_executiontrimsuffixoutput * S ((S (pftrim_index_normalization_descent_executiontrimsuffix)) * rc) + (pftrim_value_normalization_descent_executiontrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_normalization_descent_executiontrimnormal. ((((exists ff_h_pfp_normalization_descent_executiontrimnormalentry. ff_h_pfp_normalization_descent_executiontrimnormalentry + S (pftrim_leading_normalization_descent_executiontrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_normalization_descent_executiontrimnormalentry. rb = ff_q_pfp_normalization_descent_executiontrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_normalization_descent_executiontrimnormal))) /\ ((~(pftrim_leading_normalization_descent_executiontrimnormal=0))))))))))))))))))))))))))))))))) -> (((exists pfc_gap_normalization_descent_weak. pfc_gap_normalization_descent_weak+(R)=(d)) /\ ((exists pfa_gap_normalization_descent_strict. pfa_gap_normalization_descent_strict + S (R) = (S d)))))