prime_field_polynomial_division_constant_remainder_empty

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc qb qc q rb rc R. (~((p) = 1) /\ forall pfa_factor_left_normalization_constant_prime pfa_factor_right_normalization_constant_prime. (p) = pfa_factor_left_normalization_constant_prime * pfa_factor_right_normalization_constant_prime -> pfa_factor_left_normalization_constant_prime = 1 \/ pfa_factor_right_normalization_constant_prime = 1) -> (((forall fom_index_pfp_normalization_constant_executioninput. (exists fom_gap_pfp_normalization_constant_executioninput_index_bound. fom_gap_pfp_normalization_constant_executioninput_index_bound + S (fom_index_pfp_normalization_constant_executioninput) = L) -> exists fom_value_pfp_normalization_constant_executioninput. ((((exists fom_beta_height_pfp_normalization_constant_executioninput_entry. fom_beta_height_pfp_normalization_constant_executioninput_entry + S (fom_value_pfp_normalization_constant_executioninput) = S ((S (fom_index_pfp_normalization_constant_executioninput)) * ac)) /\ exists fom_beta_quotient_pfp_normalization_constant_executioninput_entry. ab = fom_beta_quotient_pfp_normalization_constant_executioninput_entry * S ((S (fom_index_pfp_normalization_constant_executioninput)) * ac) + (fom_value_pfp_normalization_constant_executioninput))) /\ (exists fom_gap_pfp_normalization_constant_executioninput_value_bound. fom_gap_pfp_normalization_constant_executioninput_value_bound + S (fom_value_pfp_normalization_constant_executioninput) = p))) /\ (((forall fom_index_pfp_normalization_constant_executiondivisor. (exists fom_gap_pfp_normalization_constant_executiondivisor_index_bound. fom_gap_pfp_normalization_constant_executiondivisor_index_bound + S (fom_index_pfp_normalization_constant_executiondivisor) = S (0)) -> exists fom_value_pfp_normalization_constant_executiondivisor. ((((exists fom_beta_height_pfp_normalization_constant_executiondivisor_entry. fom_beta_height_pfp_normalization_constant_executiondivisor_entry + S (fom_value_pfp_normalization_constant_executiondivisor) = S ((S (fom_index_pfp_normalization_constant_executiondivisor)) * bc)) /\ exists fom_beta_quotient_pfp_normalization_constant_executiondivisor_entry. bb = fom_beta_quotient_pfp_normalization_constant_executiondivisor_entry * S ((S (fom_index_pfp_normalization_constant_executiondivisor)) * bc) + (fom_value_pfp_normalization_constant_executiondivisor))) /\ (exists fom_gap_pfp_normalization_constant_executiondivisor_value_bound. fom_gap_pfp_normalization_constant_executiondivisor_value_bound + S (fom_value_pfp_normalization_constant_executiondivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_normalization_constant_executionlengthshort. pfc_gap_normalization_constant_executionlengthshort+(L)=(0))))) \/ (((~((q)=0)) /\ (((q)+(0)=(L)))))) /\ ((exists pfd_head_normalization_constant_execution pfd_inverse_normalization_constant_execution pfd_product_code_normalization_constant_execution pfd_product_scale_normalization_constant_execution pfd_residual_code_normalization_constant_execution pfd_residual_scale_normalization_constant_execution pfd_cut_normalization_constant_execution. ((((exists ff_h_pfp_normalization_constant_executionhead. ff_h_pfp_normalization_constant_executionhead + S (pfd_head_normalization_constant_execution) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_constant_executionhead. bb = ff_q_pfp_normalization_constant_executionhead * S ((S (0)) * bc) + (pfd_head_normalization_constant_execution))) /\ (((((~((pfd_head_normalization_constant_execution) = 0)) /\ ((((exists pfa_gap_normalization_constant_executioninversemultiplicationleft. pfa_gap_normalization_constant_executioninversemultiplicationleft + S (pfd_head_normalization_constant_execution) = (p)) /\ (((exists pfa_gap_normalization_constant_executioninversemultiplicationright. pfa_gap_normalization_constant_executioninversemultiplicationright + S (pfd_inverse_normalization_constant_execution) = (p)) /\ ((((exists pfa_gap_normalization_constant_executioninversemultiplicationresultbound. pfa_gap_normalization_constant_executioninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_constant_executioninversemultiplicationresultcongruence pfa_offset_right_normalization_constant_executioninversemultiplicationresultcongruence. ((pfd_head_normalization_constant_execution) * (pfd_inverse_normalization_constant_execution)) + (p) * pfa_offset_left_normalization_constant_executioninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_constant_executioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_normalization_constant_executionquotient. (exists pfa_gap_normalization_constant_executionquotientbound. pfa_gap_normalization_constant_executionquotientbound + S (pfd_index_normalization_constant_executionquotient) = (q)) -> exists pfd_value_normalization_constant_executionquotient. ((((exists ff_h_pfp_normalization_constant_executionquotiententry. ff_h_pfp_normalization_constant_executionquotiententry + S (pfd_value_normalization_constant_executionquotient) = S ((S (pfd_index_normalization_constant_executionquotient)) * qc)) /\ exists ff_q_pfp_normalization_constant_executionquotiententry. qb = ff_q_pfp_normalization_constant_executionquotiententry * S ((S (pfd_index_normalization_constant_executionquotient)) * qc) + (pfd_value_normalization_constant_executionquotient))) /\ ((exists pfd_input_normalization_constant_executionquotientstep pfd_previous_normalization_constant_executionquotientstep pfd_difference_normalization_constant_executionquotientstep. ((((exists ff_h_pfp_normalization_constant_executionquotientstepinput. ff_h_pfp_normalization_constant_executionquotientstepinput + S (pfd_input_normalization_constant_executionquotientstep) = S ((S (pfd_index_normalization_constant_executionquotient)) * ac)) /\ exists ff_q_pfp_normalization_constant_executionquotientstepinput. ab = ff_q_pfp_normalization_constant_executionquotientstepinput * S ((S (pfd_index_normalization_constant_executionquotient)) * ac) + (pfd_input_normalization_constant_executionquotientstep))) /\ (((exists pfc_terms_code_normalization_constant_executionquotientstepprevious pfc_terms_scale_normalization_constant_executionquotientstepprevious pfc_natural_sum_normalization_constant_executionquotientstepprevious. ((forall pfc_index_normalization_constant_executionquotientsteppreviousdiagonal. (exists pfa_gap_normalization_constant_executionquotientsteppreviousdiagonalbound. pfa_gap_normalization_constant_executionquotientsteppreviousdiagonalbound + S (pfc_index_normalization_constant_executionquotientsteppreviousdiagonal) = (S (pfd_index_normalization_constant_executionquotient))) -> exists pfc_value_normalization_constant_executionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_normalization_constant_executionquotientsteppreviousdiagonalentry. ff_h_pfp_normalization_constant_executionquotientsteppreviousdiagonalentry + S (pfc_value_normalization_constant_executionquotientsteppreviousdiagonal) = S ((S (pfc_index_normalization_constant_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_normalization_constant_executionquotientstepprevious)) /\ exists ff_q_pfp_normalization_constant_executionquotientsteppreviousdiagonalentry. pfc_terms_code_normalization_constant_executionquotientstepprevious = ff_q_pfp_normalization_constant_executionquotientsteppreviousdiagonalentry * S ((S (pfc_index_normalization_constant_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_normalization_constant_executionquotientstepprevious) + (pfc_value_normalization_constant_executionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_normalization_constant_executionquotientsteppreviousdiagonalterm pfc_left_normalization_constant_executionquotientsteppreviousdiagonalterm pfc_right_normalization_constant_executionquotientsteppreviousdiagonalterm. (((pfc_index_normalization_constant_executionquotientsteppreviousdiagonal)+pfc_complement_normalization_constant_executionquotientsteppreviousdiagonalterm=(pfd_index_normalization_constant_executionquotient)) /\ ((((((exists pfa_gap_normalization_constant_executionquotientsteppreviousdiagonaltermleftinside. pfa_gap_normalization_constant_executionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_normalization_constant_executionquotientsteppreviousdiagonal) = (pfd_index_normalization_constant_executionquotient)) /\ ((((exists ff_h_pfp_normalization_constant_executionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_normalization_constant_executionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_normalization_constant_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_normalization_constant_executionquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_normalization_constant_executionquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_normalization_constant_executionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_normalization_constant_executionquotientsteppreviousdiagonal)) * qc) + (pfc_left_normalization_constant_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_normalization_constant_executionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_normalization_constant_executionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_normalization_constant_executionquotient)=(pfc_index_normalization_constant_executionquotientsteppreviousdiagonal)) /\ (((pfc_left_normalization_constant_executionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalization_constant_executionquotientsteppreviousdiagonaltermrightinside. pfa_gap_normalization_constant_executionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_normalization_constant_executionquotientsteppreviousdiagonalterm) = (S (0))) /\ ((((exists ff_h_pfp_normalization_constant_executionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_normalization_constant_executionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_normalization_constant_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_normalization_constant_executionquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_normalization_constant_executionquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_normalization_constant_executionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_normalization_constant_executionquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_normalization_constant_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_normalization_constant_executionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_normalization_constant_executionquotientsteppreviousdiagonaltermrightoutside+(S (0))=(pfc_complement_normalization_constant_executionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_normalization_constant_executionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_normalization_constant_executionquotientsteppreviousdiagonal)=pfc_left_normalization_constant_executionquotientsteppreviousdiagonalterm*pfc_right_normalization_constant_executionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalization_constant_executionquotientstepprevioussum fs_v_pfc_normalization_constant_executionquotientstepprevioussum. ((((exists fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_start. fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalization_constant_executionquotientstepprevioussum)) /\ exists fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_start. fs_u_pfc_normalization_constant_executionquotientstepprevioussum = fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_normalization_constant_executionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_terminal. fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_normalization_constant_executionquotientstepprevious) = S ((S (S (pfd_index_normalization_constant_executionquotient))) * fs_v_pfc_normalization_constant_executionquotientstepprevioussum)) /\ exists fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_terminal. fs_u_pfc_normalization_constant_executionquotientstepprevioussum = fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_normalization_constant_executionquotient))) * fs_v_pfc_normalization_constant_executionquotientstepprevioussum) + (pfc_natural_sum_normalization_constant_executionquotientstepprevious))) /\ forall fs_i_pfc_normalization_constant_executionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_normalization_constant_executionquotientstepprevioussum_body_steps = S (pfd_index_normalization_constant_executionquotient)) -> exists fs_a_pfc_normalization_constant_executionquotientstepprevioussum_body_steps fs_r_pfc_normalization_constant_executionquotientstepprevioussum_body_steps fs_s_pfc_normalization_constant_executionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_summand. fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_normalization_constant_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_normalization_constant_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_normalization_constant_executionquotientstepprevious)) /\ exists fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_summand. pfc_terms_code_normalization_constant_executionquotientstepprevious = fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_normalization_constant_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_normalization_constant_executionquotientstepprevious) + (fs_a_pfc_normalization_constant_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_partial. fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_normalization_constant_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_normalization_constant_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_normalization_constant_executionquotientstepprevioussum)) /\ exists fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_partial. fs_u_pfc_normalization_constant_executionquotientstepprevioussum = fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_normalization_constant_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_normalization_constant_executionquotientstepprevioussum) + (fs_r_pfc_normalization_constant_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_successor. fs_h_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_normalization_constant_executionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_normalization_constant_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_normalization_constant_executionquotientstepprevioussum)) /\ exists fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_successor. fs_u_pfc_normalization_constant_executionquotientstepprevioussum = fs_q_pfc_normalization_constant_executionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_normalization_constant_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_normalization_constant_executionquotientstepprevioussum) + (fs_s_pfc_normalization_constant_executionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_normalization_constant_executionquotientstepprevioussum_body_steps = fs_r_pfc_normalization_constant_executionquotientstepprevioussum_body_steps + fs_a_pfc_normalization_constant_executionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_normalization_constant_executionquotientsteppreviousresiduebound. pfa_gap_normalization_constant_executionquotientsteppreviousresiduebound + S (pfd_previous_normalization_constant_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_normalization_constant_executionquotientsteppreviousresiduecongruence pfa_offset_right_normalization_constant_executionquotientsteppreviousresiduecongruence. (pfc_natural_sum_normalization_constant_executionquotientstepprevious) + (p) * pfa_offset_left_normalization_constant_executionquotientsteppreviousresiduecongruence = (pfd_previous_normalization_constant_executionquotientstep) + (p) * pfa_offset_right_normalization_constant_executionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_normalization_constant_executionquotientstepsubtractleft. pfa_gap_normalization_constant_executionquotientstepsubtractleft + S (pfd_previous_normalization_constant_executionquotientstep) = (p)) /\ (((exists pfa_gap_normalization_constant_executionquotientstepsubtractright. pfa_gap_normalization_constant_executionquotientstepsubtractright + S (pfd_difference_normalization_constant_executionquotientstep) = (p)) /\ ((((exists pfa_gap_normalization_constant_executionquotientstepsubtractresultbound. pfa_gap_normalization_constant_executionquotientstepsubtractresultbound + S (pfd_input_normalization_constant_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_normalization_constant_executionquotientstepsubtractresultcongruence pfa_offset_right_normalization_constant_executionquotientstepsubtractresultcongruence. ((pfd_previous_normalization_constant_executionquotientstep) + (pfd_difference_normalization_constant_executionquotientstep)) + (p) * pfa_offset_left_normalization_constant_executionquotientstepsubtractresultcongruence = (pfd_input_normalization_constant_executionquotientstep) + (p) * pfa_offset_right_normalization_constant_executionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_normalization_constant_executionquotientstepmultiplyleft. pfa_gap_normalization_constant_executionquotientstepmultiplyleft + S (pfd_inverse_normalization_constant_execution) = (p)) /\ (((exists pfa_gap_normalization_constant_executionquotientstepmultiplyright. pfa_gap_normalization_constant_executionquotientstepmultiplyright + S (pfd_difference_normalization_constant_executionquotientstep) = (p)) /\ ((((exists pfa_gap_normalization_constant_executionquotientstepmultiplyresultbound. pfa_gap_normalization_constant_executionquotientstepmultiplyresultbound + S (pfd_value_normalization_constant_executionquotient) = (p)) /\ ((exists pfa_offset_left_normalization_constant_executionquotientstepmultiplyresultcongruence pfa_offset_right_normalization_constant_executionquotientstepmultiplyresultcongruence. ((pfd_inverse_normalization_constant_execution) * (pfd_difference_normalization_constant_executionquotientstep)) + (p) * pfa_offset_left_normalization_constant_executionquotientstepmultiplyresultcongruence = (pfd_value_normalization_constant_executionquotient) + (p) * pfa_offset_right_normalization_constant_executionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_normalization_constant_executionproduct. (exists pfa_gap_normalization_constant_executionproductbound. pfa_gap_normalization_constant_executionproductbound + S (pfc_index_normalization_constant_executionproduct) = (L)) -> exists pfc_value_normalization_constant_executionproduct. ((((exists ff_h_pfp_normalization_constant_executionproductentry. ff_h_pfp_normalization_constant_executionproductentry + S (pfc_value_normalization_constant_executionproduct) = S ((S (pfc_index_normalization_constant_executionproduct)) * pfd_product_scale_normalization_constant_execution)) /\ exists ff_q_pfp_normalization_constant_executionproductentry. pfd_product_code_normalization_constant_execution = ff_q_pfp_normalization_constant_executionproductentry * S ((S (pfc_index_normalization_constant_executionproduct)) * pfd_product_scale_normalization_constant_execution) + (pfc_value_normalization_constant_executionproduct))) /\ ((exists pfc_terms_code_normalization_constant_executionproductcoefficient pfc_terms_scale_normalization_constant_executionproductcoefficient pfc_natural_sum_normalization_constant_executionproductcoefficient. ((forall pfc_index_normalization_constant_executionproductcoefficientdiagonal. (exists pfa_gap_normalization_constant_executionproductcoefficientdiagonalbound. pfa_gap_normalization_constant_executionproductcoefficientdiagonalbound + S (pfc_index_normalization_constant_executionproductcoefficientdiagonal) = (S (pfc_index_normalization_constant_executionproduct))) -> exists pfc_value_normalization_constant_executionproductcoefficientdiagonal. ((((exists ff_h_pfp_normalization_constant_executionproductcoefficientdiagonalentry. ff_h_pfp_normalization_constant_executionproductcoefficientdiagonalentry + S (pfc_value_normalization_constant_executionproductcoefficientdiagonal) = S ((S (pfc_index_normalization_constant_executionproductcoefficientdiagonal)) * pfc_terms_scale_normalization_constant_executionproductcoefficient)) /\ exists ff_q_pfp_normalization_constant_executionproductcoefficientdiagonalentry. pfc_terms_code_normalization_constant_executionproductcoefficient = ff_q_pfp_normalization_constant_executionproductcoefficientdiagonalentry * S ((S (pfc_index_normalization_constant_executionproductcoefficientdiagonal)) * pfc_terms_scale_normalization_constant_executionproductcoefficient) + (pfc_value_normalization_constant_executionproductcoefficientdiagonal))) /\ ((exists pfc_complement_normalization_constant_executionproductcoefficientdiagonalterm pfc_left_normalization_constant_executionproductcoefficientdiagonalterm pfc_right_normalization_constant_executionproductcoefficientdiagonalterm. (((pfc_index_normalization_constant_executionproductcoefficientdiagonal)+pfc_complement_normalization_constant_executionproductcoefficientdiagonalterm=(pfc_index_normalization_constant_executionproduct)) /\ ((((((exists pfa_gap_normalization_constant_executionproductcoefficientdiagonaltermleftinside. pfa_gap_normalization_constant_executionproductcoefficientdiagonaltermleftinside + S (pfc_index_normalization_constant_executionproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_normalization_constant_executionproductcoefficientdiagonaltermleftentry. ff_h_pfp_normalization_constant_executionproductcoefficientdiagonaltermleftentry + S (pfc_left_normalization_constant_executionproductcoefficientdiagonalterm) = S ((S (pfc_index_normalization_constant_executionproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_normalization_constant_executionproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_normalization_constant_executionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_normalization_constant_executionproductcoefficientdiagonal)) * qc) + (pfc_left_normalization_constant_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_constant_executionproductcoefficientdiagonaltermleftoutside. pfc_gap_normalization_constant_executionproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_normalization_constant_executionproductcoefficientdiagonal)) /\ (((pfc_left_normalization_constant_executionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalization_constant_executionproductcoefficientdiagonaltermrightinside. pfa_gap_normalization_constant_executionproductcoefficientdiagonaltermrightinside + S (pfc_complement_normalization_constant_executionproductcoefficientdiagonalterm) = (S (0))) /\ ((((exists ff_h_pfp_normalization_constant_executionproductcoefficientdiagonaltermrightentry. ff_h_pfp_normalization_constant_executionproductcoefficientdiagonaltermrightentry + S (pfc_right_normalization_constant_executionproductcoefficientdiagonalterm) = S ((S (pfc_complement_normalization_constant_executionproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_normalization_constant_executionproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_normalization_constant_executionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalization_constant_executionproductcoefficientdiagonalterm)) * bc) + (pfc_right_normalization_constant_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_constant_executionproductcoefficientdiagonaltermrightoutside. pfc_gap_normalization_constant_executionproductcoefficientdiagonaltermrightoutside+(S (0))=(pfc_complement_normalization_constant_executionproductcoefficientdiagonalterm)) /\ (((pfc_right_normalization_constant_executionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalization_constant_executionproductcoefficientdiagonal)=pfc_left_normalization_constant_executionproductcoefficientdiagonalterm*pfc_right_normalization_constant_executionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalization_constant_executionproductcoefficientsum fs_v_pfc_normalization_constant_executionproductcoefficientsum. ((((exists fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_start. fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalization_constant_executionproductcoefficientsum)) /\ exists fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_start. fs_u_pfc_normalization_constant_executionproductcoefficientsum = fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalization_constant_executionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_terminal. fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_terminal + S (pfc_natural_sum_normalization_constant_executionproductcoefficient) = S ((S (S (pfc_index_normalization_constant_executionproduct))) * fs_v_pfc_normalization_constant_executionproductcoefficientsum)) /\ exists fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_terminal. fs_u_pfc_normalization_constant_executionproductcoefficientsum = fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_normalization_constant_executionproduct))) * fs_v_pfc_normalization_constant_executionproductcoefficientsum) + (pfc_natural_sum_normalization_constant_executionproductcoefficient))) /\ forall fs_i_pfc_normalization_constant_executionproductcoefficientsum_body_steps. (exists fs_lt_pfc_normalization_constant_executionproductcoefficientsum_body_steps_bound. fs_lt_pfc_normalization_constant_executionproductcoefficientsum_body_steps_bound + S fs_i_pfc_normalization_constant_executionproductcoefficientsum_body_steps = S (pfc_index_normalization_constant_executionproduct)) -> exists fs_a_pfc_normalization_constant_executionproductcoefficientsum_body_steps fs_r_pfc_normalization_constant_executionproductcoefficientsum_body_steps fs_s_pfc_normalization_constant_executionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_steps_summand. fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_normalization_constant_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_constant_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_normalization_constant_executionproductcoefficient)) /\ exists fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_steps_summand. pfc_terms_code_normalization_constant_executionproductcoefficient = fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalization_constant_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_normalization_constant_executionproductcoefficient) + (fs_a_pfc_normalization_constant_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_steps_partial. fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_normalization_constant_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_constant_executionproductcoefficientsum_body_steps)) * fs_v_pfc_normalization_constant_executionproductcoefficientsum)) /\ exists fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_steps_partial. fs_u_pfc_normalization_constant_executionproductcoefficientsum = fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalization_constant_executionproductcoefficientsum_body_steps)) * fs_v_pfc_normalization_constant_executionproductcoefficientsum) + (fs_r_pfc_normalization_constant_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_steps_successor. fs_h_pfc_normalization_constant_executionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_normalization_constant_executionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalization_constant_executionproductcoefficientsum_body_steps)) * fs_v_pfc_normalization_constant_executionproductcoefficientsum)) /\ exists fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_steps_successor. fs_u_pfc_normalization_constant_executionproductcoefficientsum = fs_q_pfc_normalization_constant_executionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalization_constant_executionproductcoefficientsum_body_steps)) * fs_v_pfc_normalization_constant_executionproductcoefficientsum) + (fs_s_pfc_normalization_constant_executionproductcoefficientsum_body_steps))) /\ fs_s_pfc_normalization_constant_executionproductcoefficientsum_body_steps = fs_r_pfc_normalization_constant_executionproductcoefficientsum_body_steps + fs_a_pfc_normalization_constant_executionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalization_constant_executionproductcoefficientresiduebound. pfa_gap_normalization_constant_executionproductcoefficientresiduebound + S (pfc_value_normalization_constant_executionproduct) = (p)) /\ ((exists pfa_offset_left_normalization_constant_executionproductcoefficientresiduecongruence pfa_offset_right_normalization_constant_executionproductcoefficientresiduecongruence. (pfc_natural_sum_normalization_constant_executionproductcoefficient) + (p) * pfa_offset_left_normalization_constant_executionproductcoefficientresiduecongruence = (pfc_value_normalization_constant_executionproduct) + (p) * pfa_offset_right_normalization_constant_executionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_normalization_constant_executiondifference. (exists pfa_gap_normalization_constant_executiondifferenceindex. pfa_gap_normalization_constant_executiondifferenceindex + S (pfs_index_normalization_constant_executiondifference) = (L)) -> exists pfs_left_normalization_constant_executiondifference pfs_right_normalization_constant_executiondifference pfs_result_normalization_constant_executiondifference. ((((exists ff_h_pfp_normalization_constant_executiondifferenceleft. ff_h_pfp_normalization_constant_executiondifferenceleft + S (pfs_left_normalization_constant_executiondifference) = S ((S (pfs_index_normalization_constant_executiondifference)) * ac)) /\ exists ff_q_pfp_normalization_constant_executiondifferenceleft. ab = ff_q_pfp_normalization_constant_executiondifferenceleft * S ((S (pfs_index_normalization_constant_executiondifference)) * ac) + (pfs_left_normalization_constant_executiondifference))) /\ (((((exists ff_h_pfp_normalization_constant_executiondifferenceright. ff_h_pfp_normalization_constant_executiondifferenceright + S (pfs_right_normalization_constant_executiondifference) = S ((S (pfs_index_normalization_constant_executiondifference)) * pfd_product_scale_normalization_constant_execution)) /\ exists ff_q_pfp_normalization_constant_executiondifferenceright. pfd_product_code_normalization_constant_execution = ff_q_pfp_normalization_constant_executiondifferenceright * S ((S (pfs_index_normalization_constant_executiondifference)) * pfd_product_scale_normalization_constant_execution) + (pfs_right_normalization_constant_executiondifference))) /\ (((((exists ff_h_pfp_normalization_constant_executiondifferenceresult. ff_h_pfp_normalization_constant_executiondifferenceresult + S (pfs_result_normalization_constant_executiondifference) = S ((S (pfs_index_normalization_constant_executiondifference)) * pfd_residual_scale_normalization_constant_execution)) /\ exists ff_q_pfp_normalization_constant_executiondifferenceresult. pfd_residual_code_normalization_constant_execution = ff_q_pfp_normalization_constant_executiondifferenceresult * S ((S (pfs_index_normalization_constant_executiondifference)) * pfd_residual_scale_normalization_constant_execution) + (pfs_result_normalization_constant_executiondifference))) /\ ((((exists pfa_gap_normalization_constant_executiondifferenceoperationleft. pfa_gap_normalization_constant_executiondifferenceoperationleft + S (pfs_right_normalization_constant_executiondifference) = (p)) /\ (((exists pfa_gap_normalization_constant_executiondifferenceoperationright. pfa_gap_normalization_constant_executiondifferenceoperationright + S (pfs_result_normalization_constant_executiondifference) = (p)) /\ ((((exists pfa_gap_normalization_constant_executiondifferenceoperationresultbound. pfa_gap_normalization_constant_executiondifferenceoperationresultbound + S (pfs_left_normalization_constant_executiondifference) = (p)) /\ ((exists pfa_offset_left_normalization_constant_executiondifferenceoperationresultcongruence pfa_offset_right_normalization_constant_executiondifferenceoperationresultcongruence. ((pfs_right_normalization_constant_executiondifference) + (pfs_result_normalization_constant_executiondifference)) + (p) * pfa_offset_left_normalization_constant_executiondifferenceoperationresultcongruence = (pfs_left_normalization_constant_executiondifference) + (p) * pfa_offset_right_normalization_constant_executiondifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_normalization_constant_execution)+(R)) /\ (((forall fom_index_pfp_normalization_constant_executiontriminput. (exists fom_gap_pfp_normalization_constant_executiontriminput_index_bound. fom_gap_pfp_normalization_constant_executiontriminput_index_bound + S (fom_index_pfp_normalization_constant_executiontriminput) = L) -> exists fom_value_pfp_normalization_constant_executiontriminput. ((((exists fom_beta_height_pfp_normalization_constant_executiontriminput_entry. fom_beta_height_pfp_normalization_constant_executiontriminput_entry + S (fom_value_pfp_normalization_constant_executiontriminput) = S ((S (fom_index_pfp_normalization_constant_executiontriminput)) * pfd_residual_scale_normalization_constant_execution)) /\ exists fom_beta_quotient_pfp_normalization_constant_executiontriminput_entry. pfd_residual_code_normalization_constant_execution = fom_beta_quotient_pfp_normalization_constant_executiontriminput_entry * S ((S (fom_index_pfp_normalization_constant_executiontriminput)) * pfd_residual_scale_normalization_constant_execution) + (fom_value_pfp_normalization_constant_executiontriminput))) /\ (exists fom_gap_pfp_normalization_constant_executiontriminput_value_bound. fom_gap_pfp_normalization_constant_executiontriminput_value_bound + S (fom_value_pfp_normalization_constant_executiontriminput) = p))) /\ (((forall pfp_repeat_index_normalization_constant_executiontrimremoved. (exists pfa_gap_normalization_constant_executiontrimremovedindex. pfa_gap_normalization_constant_executiontrimremovedindex + S (pfp_repeat_index_normalization_constant_executiontrimremoved) = (pfd_cut_normalization_constant_execution)) -> (((exists ff_h_pfp_normalization_constant_executiontrimremovedentry. ff_h_pfp_normalization_constant_executiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_normalization_constant_executiontrimremoved)) * pfd_residual_scale_normalization_constant_execution)) /\ exists ff_q_pfp_normalization_constant_executiontrimremovedentry. pfd_residual_code_normalization_constant_execution = ff_q_pfp_normalization_constant_executiontrimremovedentry * S ((S (pfp_repeat_index_normalization_constant_executiontrimremoved)) * pfd_residual_scale_normalization_constant_execution) + (0)))) /\ (((forall pftrim_index_normalization_constant_executiontrimsuffix pftrim_value_normalization_constant_executiontrimsuffix. (exists pfa_gap_normalization_constant_executiontrimsuffixbound. pfa_gap_normalization_constant_executiontrimsuffixbound + S (pftrim_index_normalization_constant_executiontrimsuffix) = (R)) -> (((exists ff_h_pfp_normalization_constant_executiontrimsuffixsource. ff_h_pfp_normalization_constant_executiontrimsuffixsource + S (pftrim_value_normalization_constant_executiontrimsuffix) = S ((S ((pfd_cut_normalization_constant_execution)+pftrim_index_normalization_constant_executiontrimsuffix)) * pfd_residual_scale_normalization_constant_execution)) /\ exists ff_q_pfp_normalization_constant_executiontrimsuffixsource. pfd_residual_code_normalization_constant_execution = ff_q_pfp_normalization_constant_executiontrimsuffixsource * S ((S ((pfd_cut_normalization_constant_execution)+pftrim_index_normalization_constant_executiontrimsuffix)) * pfd_residual_scale_normalization_constant_execution) + (pftrim_value_normalization_constant_executiontrimsuffix))) -> (((exists ff_h_pfp_normalization_constant_executiontrimsuffixoutput. ff_h_pfp_normalization_constant_executiontrimsuffixoutput + S (pftrim_value_normalization_constant_executiontrimsuffix) = S ((S (pftrim_index_normalization_constant_executiontrimsuffix)) * rc)) /\ exists ff_q_pfp_normalization_constant_executiontrimsuffixoutput. rb = ff_q_pfp_normalization_constant_executiontrimsuffixoutput * S ((S (pftrim_index_normalization_constant_executiontrimsuffix)) * rc) + (pftrim_value_normalization_constant_executiontrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_normalization_constant_executiontrimnormal. ((((exists ff_h_pfp_normalization_constant_executiontrimnormalentry. ff_h_pfp_normalization_constant_executiontrimnormalentry + S (pftrim_leading_normalization_constant_executiontrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_normalization_constant_executiontrimnormalentry. rb = ff_q_pfp_normalization_constant_executiontrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_normalization_constant_executiontrimnormal))) /\ ((~(pftrim_leading_normalization_constant_executiontrimnormal=0))))))))))))))))))))))))))))))))) -> (R=0)