prime_field_polynomial_division_remainder_bounded

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc d qb qc q rb rc R. (((forall fom_index_pfp_gcd_remainder_executioninput. (exists fom_gap_pfp_gcd_remainder_executioninput_index_bound. fom_gap_pfp_gcd_remainder_executioninput_index_bound + S (fom_index_pfp_gcd_remainder_executioninput) = L) -> exists fom_value_pfp_gcd_remainder_executioninput. ((((exists fom_beta_height_pfp_gcd_remainder_executioninput_entry. fom_beta_height_pfp_gcd_remainder_executioninput_entry + S (fom_value_pfp_gcd_remainder_executioninput) = S ((S (fom_index_pfp_gcd_remainder_executioninput)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_remainder_executioninput_entry. ab = fom_beta_quotient_pfp_gcd_remainder_executioninput_entry * S ((S (fom_index_pfp_gcd_remainder_executioninput)) * ac) + (fom_value_pfp_gcd_remainder_executioninput))) /\ (exists fom_gap_pfp_gcd_remainder_executioninput_value_bound. fom_gap_pfp_gcd_remainder_executioninput_value_bound + S (fom_value_pfp_gcd_remainder_executioninput) = p))) /\ (((forall fom_index_pfp_gcd_remainder_executiondivisor. (exists fom_gap_pfp_gcd_remainder_executiondivisor_index_bound. fom_gap_pfp_gcd_remainder_executiondivisor_index_bound + S (fom_index_pfp_gcd_remainder_executiondivisor) = S (d)) -> exists fom_value_pfp_gcd_remainder_executiondivisor. ((((exists fom_beta_height_pfp_gcd_remainder_executiondivisor_entry. fom_beta_height_pfp_gcd_remainder_executiondivisor_entry + S (fom_value_pfp_gcd_remainder_executiondivisor) = S ((S (fom_index_pfp_gcd_remainder_executiondivisor)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_remainder_executiondivisor_entry. bb = fom_beta_quotient_pfp_gcd_remainder_executiondivisor_entry * S ((S (fom_index_pfp_gcd_remainder_executiondivisor)) * bc) + (fom_value_pfp_gcd_remainder_executiondivisor))) /\ (exists fom_gap_pfp_gcd_remainder_executiondivisor_value_bound. fom_gap_pfp_gcd_remainder_executiondivisor_value_bound + S (fom_value_pfp_gcd_remainder_executiondivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_gcd_remainder_executionlengthshort. pfc_gap_gcd_remainder_executionlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_gcd_remainder_execution pfd_inverse_gcd_remainder_execution pfd_product_code_gcd_remainder_execution pfd_product_scale_gcd_remainder_execution pfd_residual_code_gcd_remainder_execution pfd_residual_scale_gcd_remainder_execution pfd_cut_gcd_remainder_execution. ((((exists ff_h_pfp_gcd_remainder_executionhead. ff_h_pfp_gcd_remainder_executionhead + S (pfd_head_gcd_remainder_execution) = S ((S (0)) * bc)) /\ exists ff_q_pfp_gcd_remainder_executionhead. bb = ff_q_pfp_gcd_remainder_executionhead * S ((S (0)) * bc) + (pfd_head_gcd_remainder_execution))) /\ (((((~((pfd_head_gcd_remainder_execution) = 0)) /\ ((((exists pfa_gap_gcd_remainder_executioninversemultiplicationleft. pfa_gap_gcd_remainder_executioninversemultiplicationleft + S (pfd_head_gcd_remainder_execution) = (p)) /\ (((exists pfa_gap_gcd_remainder_executioninversemultiplicationright. pfa_gap_gcd_remainder_executioninversemultiplicationright + S (pfd_inverse_gcd_remainder_execution) = (p)) /\ ((((exists pfa_gap_gcd_remainder_executioninversemultiplicationresultbound. pfa_gap_gcd_remainder_executioninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_gcd_remainder_executioninversemultiplicationresultcongruence pfa_offset_right_gcd_remainder_executioninversemultiplicationresultcongruence. ((pfd_head_gcd_remainder_execution) * (pfd_inverse_gcd_remainder_execution)) + (p) * pfa_offset_left_gcd_remainder_executioninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_gcd_remainder_executioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_gcd_remainder_executionquotient. (exists pfa_gap_gcd_remainder_executionquotientbound. pfa_gap_gcd_remainder_executionquotientbound + S (pfd_index_gcd_remainder_executionquotient) = (q)) -> exists pfd_value_gcd_remainder_executionquotient. ((((exists ff_h_pfp_gcd_remainder_executionquotiententry. ff_h_pfp_gcd_remainder_executionquotiententry + S (pfd_value_gcd_remainder_executionquotient) = S ((S (pfd_index_gcd_remainder_executionquotient)) * qc)) /\ exists ff_q_pfp_gcd_remainder_executionquotiententry. qb = ff_q_pfp_gcd_remainder_executionquotiententry * S ((S (pfd_index_gcd_remainder_executionquotient)) * qc) + (pfd_value_gcd_remainder_executionquotient))) /\ ((exists pfd_input_gcd_remainder_executionquotientstep pfd_previous_gcd_remainder_executionquotientstep pfd_difference_gcd_remainder_executionquotientstep. ((((exists ff_h_pfp_gcd_remainder_executionquotientstepinput. ff_h_pfp_gcd_remainder_executionquotientstepinput + S (pfd_input_gcd_remainder_executionquotientstep) = S ((S (pfd_index_gcd_remainder_executionquotient)) * ac)) /\ exists ff_q_pfp_gcd_remainder_executionquotientstepinput. ab = ff_q_pfp_gcd_remainder_executionquotientstepinput * S ((S (pfd_index_gcd_remainder_executionquotient)) * ac) + (pfd_input_gcd_remainder_executionquotientstep))) /\ (((exists pfc_terms_code_gcd_remainder_executionquotientstepprevious pfc_terms_scale_gcd_remainder_executionquotientstepprevious pfc_natural_sum_gcd_remainder_executionquotientstepprevious. ((forall pfc_index_gcd_remainder_executionquotientsteppreviousdiagonal. (exists pfa_gap_gcd_remainder_executionquotientsteppreviousdiagonalbound. pfa_gap_gcd_remainder_executionquotientsteppreviousdiagonalbound + S (pfc_index_gcd_remainder_executionquotientsteppreviousdiagonal) = (S (pfd_index_gcd_remainder_executionquotient))) -> exists pfc_value_gcd_remainder_executionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_gcd_remainder_executionquotientsteppreviousdiagonalentry. ff_h_pfp_gcd_remainder_executionquotientsteppreviousdiagonalentry + S (pfc_value_gcd_remainder_executionquotientsteppreviousdiagonal) = S ((S (pfc_index_gcd_remainder_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_gcd_remainder_executionquotientstepprevious)) /\ exists ff_q_pfp_gcd_remainder_executionquotientsteppreviousdiagonalentry. pfc_terms_code_gcd_remainder_executionquotientstepprevious = ff_q_pfp_gcd_remainder_executionquotientsteppreviousdiagonalentry * S ((S (pfc_index_gcd_remainder_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_gcd_remainder_executionquotientstepprevious) + (pfc_value_gcd_remainder_executionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_gcd_remainder_executionquotientsteppreviousdiagonalterm pfc_left_gcd_remainder_executionquotientsteppreviousdiagonalterm pfc_right_gcd_remainder_executionquotientsteppreviousdiagonalterm. (((pfc_index_gcd_remainder_executionquotientsteppreviousdiagonal)+pfc_complement_gcd_remainder_executionquotientsteppreviousdiagonalterm=(pfd_index_gcd_remainder_executionquotient)) /\ ((((((exists pfa_gap_gcd_remainder_executionquotientsteppreviousdiagonaltermleftinside. pfa_gap_gcd_remainder_executionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_gcd_remainder_executionquotientsteppreviousdiagonal) = (pfd_index_gcd_remainder_executionquotient)) /\ ((((exists ff_h_pfp_gcd_remainder_executionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_gcd_remainder_executionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_gcd_remainder_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_gcd_remainder_executionquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_gcd_remainder_executionquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_gcd_remainder_executionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_gcd_remainder_executionquotientsteppreviousdiagonal)) * qc) + (pfc_left_gcd_remainder_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_gcd_remainder_executionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_gcd_remainder_executionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_gcd_remainder_executionquotient)=(pfc_index_gcd_remainder_executionquotientsteppreviousdiagonal)) /\ (((pfc_left_gcd_remainder_executionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_remainder_executionquotientsteppreviousdiagonaltermrightinside. pfa_gap_gcd_remainder_executionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_gcd_remainder_executionquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_gcd_remainder_executionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_gcd_remainder_executionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_gcd_remainder_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_gcd_remainder_executionquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_remainder_executionquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_gcd_remainder_executionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_gcd_remainder_executionquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_gcd_remainder_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_gcd_remainder_executionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_gcd_remainder_executionquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_gcd_remainder_executionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_gcd_remainder_executionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_gcd_remainder_executionquotientsteppreviousdiagonal)=pfc_left_gcd_remainder_executionquotientsteppreviousdiagonalterm*pfc_right_gcd_remainder_executionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_remainder_executionquotientstepprevioussum fs_v_pfc_gcd_remainder_executionquotientstepprevioussum. ((((exists fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_start. fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_remainder_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_start. fs_u_pfc_gcd_remainder_executionquotientstepprevioussum = fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_gcd_remainder_executionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_terminal. fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_gcd_remainder_executionquotientstepprevious) = S ((S (S (pfd_index_gcd_remainder_executionquotient))) * fs_v_pfc_gcd_remainder_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_terminal. fs_u_pfc_gcd_remainder_executionquotientstepprevioussum = fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_gcd_remainder_executionquotient))) * fs_v_pfc_gcd_remainder_executionquotientstepprevioussum) + (pfc_natural_sum_gcd_remainder_executionquotientstepprevious))) /\ forall fs_i_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps = S (pfd_index_gcd_remainder_executionquotient)) -> exists fs_a_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps fs_r_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps fs_s_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_summand. fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_gcd_remainder_executionquotientstepprevious)) /\ exists fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_summand. pfc_terms_code_gcd_remainder_executionquotientstepprevious = fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_gcd_remainder_executionquotientstepprevious) + (fs_a_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_partial. fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_remainder_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_partial. fs_u_pfc_gcd_remainder_executionquotientstepprevioussum = fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_remainder_executionquotientstepprevioussum) + (fs_r_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_successor. fs_h_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_remainder_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_successor. fs_u_pfc_gcd_remainder_executionquotientstepprevioussum = fs_q_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_remainder_executionquotientstepprevioussum) + (fs_s_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps = fs_r_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps + fs_a_pfc_gcd_remainder_executionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_gcd_remainder_executionquotientsteppreviousresiduebound. pfa_gap_gcd_remainder_executionquotientsteppreviousresiduebound + S (pfd_previous_gcd_remainder_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_gcd_remainder_executionquotientsteppreviousresiduecongruence pfa_offset_right_gcd_remainder_executionquotientsteppreviousresiduecongruence. (pfc_natural_sum_gcd_remainder_executionquotientstepprevious) + (p) * pfa_offset_left_gcd_remainder_executionquotientsteppreviousresiduecongruence = (pfd_previous_gcd_remainder_executionquotientstep) + (p) * pfa_offset_right_gcd_remainder_executionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_gcd_remainder_executionquotientstepsubtractleft. pfa_gap_gcd_remainder_executionquotientstepsubtractleft + S (pfd_previous_gcd_remainder_executionquotientstep) = (p)) /\ (((exists pfa_gap_gcd_remainder_executionquotientstepsubtractright. pfa_gap_gcd_remainder_executionquotientstepsubtractright + S (pfd_difference_gcd_remainder_executionquotientstep) = (p)) /\ ((((exists pfa_gap_gcd_remainder_executionquotientstepsubtractresultbound. pfa_gap_gcd_remainder_executionquotientstepsubtractresultbound + S (pfd_input_gcd_remainder_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_gcd_remainder_executionquotientstepsubtractresultcongruence pfa_offset_right_gcd_remainder_executionquotientstepsubtractresultcongruence. ((pfd_previous_gcd_remainder_executionquotientstep) + (pfd_difference_gcd_remainder_executionquotientstep)) + (p) * pfa_offset_left_gcd_remainder_executionquotientstepsubtractresultcongruence = (pfd_input_gcd_remainder_executionquotientstep) + (p) * pfa_offset_right_gcd_remainder_executionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_gcd_remainder_executionquotientstepmultiplyleft. pfa_gap_gcd_remainder_executionquotientstepmultiplyleft + S (pfd_inverse_gcd_remainder_execution) = (p)) /\ (((exists pfa_gap_gcd_remainder_executionquotientstepmultiplyright. pfa_gap_gcd_remainder_executionquotientstepmultiplyright + S (pfd_difference_gcd_remainder_executionquotientstep) = (p)) /\ ((((exists pfa_gap_gcd_remainder_executionquotientstepmultiplyresultbound. pfa_gap_gcd_remainder_executionquotientstepmultiplyresultbound + S (pfd_value_gcd_remainder_executionquotient) = (p)) /\ ((exists pfa_offset_left_gcd_remainder_executionquotientstepmultiplyresultcongruence pfa_offset_right_gcd_remainder_executionquotientstepmultiplyresultcongruence. ((pfd_inverse_gcd_remainder_execution) * (pfd_difference_gcd_remainder_executionquotientstep)) + (p) * pfa_offset_left_gcd_remainder_executionquotientstepmultiplyresultcongruence = (pfd_value_gcd_remainder_executionquotient) + (p) * pfa_offset_right_gcd_remainder_executionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_gcd_remainder_executionproduct. (exists pfa_gap_gcd_remainder_executionproductbound. pfa_gap_gcd_remainder_executionproductbound + S (pfc_index_gcd_remainder_executionproduct) = (L)) -> exists pfc_value_gcd_remainder_executionproduct. ((((exists ff_h_pfp_gcd_remainder_executionproductentry. ff_h_pfp_gcd_remainder_executionproductentry + S (pfc_value_gcd_remainder_executionproduct) = S ((S (pfc_index_gcd_remainder_executionproduct)) * pfd_product_scale_gcd_remainder_execution)) /\ exists ff_q_pfp_gcd_remainder_executionproductentry. pfd_product_code_gcd_remainder_execution = ff_q_pfp_gcd_remainder_executionproductentry * S ((S (pfc_index_gcd_remainder_executionproduct)) * pfd_product_scale_gcd_remainder_execution) + (pfc_value_gcd_remainder_executionproduct))) /\ ((exists pfc_terms_code_gcd_remainder_executionproductcoefficient pfc_terms_scale_gcd_remainder_executionproductcoefficient pfc_natural_sum_gcd_remainder_executionproductcoefficient. ((forall pfc_index_gcd_remainder_executionproductcoefficientdiagonal. (exists pfa_gap_gcd_remainder_executionproductcoefficientdiagonalbound. pfa_gap_gcd_remainder_executionproductcoefficientdiagonalbound + S (pfc_index_gcd_remainder_executionproductcoefficientdiagonal) = (S (pfc_index_gcd_remainder_executionproduct))) -> exists pfc_value_gcd_remainder_executionproductcoefficientdiagonal. ((((exists ff_h_pfp_gcd_remainder_executionproductcoefficientdiagonalentry. ff_h_pfp_gcd_remainder_executionproductcoefficientdiagonalentry + S (pfc_value_gcd_remainder_executionproductcoefficientdiagonal) = S ((S (pfc_index_gcd_remainder_executionproductcoefficientdiagonal)) * pfc_terms_scale_gcd_remainder_executionproductcoefficient)) /\ exists ff_q_pfp_gcd_remainder_executionproductcoefficientdiagonalentry. pfc_terms_code_gcd_remainder_executionproductcoefficient = ff_q_pfp_gcd_remainder_executionproductcoefficientdiagonalentry * S ((S (pfc_index_gcd_remainder_executionproductcoefficientdiagonal)) * pfc_terms_scale_gcd_remainder_executionproductcoefficient) + (pfc_value_gcd_remainder_executionproductcoefficientdiagonal))) /\ ((exists pfc_complement_gcd_remainder_executionproductcoefficientdiagonalterm pfc_left_gcd_remainder_executionproductcoefficientdiagonalterm pfc_right_gcd_remainder_executionproductcoefficientdiagonalterm. (((pfc_index_gcd_remainder_executionproductcoefficientdiagonal)+pfc_complement_gcd_remainder_executionproductcoefficientdiagonalterm=(pfc_index_gcd_remainder_executionproduct)) /\ ((((((exists pfa_gap_gcd_remainder_executionproductcoefficientdiagonaltermleftinside. pfa_gap_gcd_remainder_executionproductcoefficientdiagonaltermleftinside + S (pfc_index_gcd_remainder_executionproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_gcd_remainder_executionproductcoefficientdiagonaltermleftentry. ff_h_pfp_gcd_remainder_executionproductcoefficientdiagonaltermleftentry + S (pfc_left_gcd_remainder_executionproductcoefficientdiagonalterm) = S ((S (pfc_index_gcd_remainder_executionproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_gcd_remainder_executionproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_gcd_remainder_executionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_remainder_executionproductcoefficientdiagonal)) * qc) + (pfc_left_gcd_remainder_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_remainder_executionproductcoefficientdiagonaltermleftoutside. pfc_gap_gcd_remainder_executionproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_gcd_remainder_executionproductcoefficientdiagonal)) /\ (((pfc_left_gcd_remainder_executionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_remainder_executionproductcoefficientdiagonaltermrightinside. pfa_gap_gcd_remainder_executionproductcoefficientdiagonaltermrightinside + S (pfc_complement_gcd_remainder_executionproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_gcd_remainder_executionproductcoefficientdiagonaltermrightentry. ff_h_pfp_gcd_remainder_executionproductcoefficientdiagonaltermrightentry + S (pfc_right_gcd_remainder_executionproductcoefficientdiagonalterm) = S ((S (pfc_complement_gcd_remainder_executionproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_remainder_executionproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_remainder_executionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_remainder_executionproductcoefficientdiagonalterm)) * bc) + (pfc_right_gcd_remainder_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_remainder_executionproductcoefficientdiagonaltermrightoutside. pfc_gap_gcd_remainder_executionproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_gcd_remainder_executionproductcoefficientdiagonalterm)) /\ (((pfc_right_gcd_remainder_executionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_remainder_executionproductcoefficientdiagonal)=pfc_left_gcd_remainder_executionproductcoefficientdiagonalterm*pfc_right_gcd_remainder_executionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_remainder_executionproductcoefficientsum fs_v_pfc_gcd_remainder_executionproductcoefficientsum. ((((exists fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_start. fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_remainder_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_start. fs_u_pfc_gcd_remainder_executionproductcoefficientsum = fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_remainder_executionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_terminal. fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_terminal + S (pfc_natural_sum_gcd_remainder_executionproductcoefficient) = S ((S (S (pfc_index_gcd_remainder_executionproduct))) * fs_v_pfc_gcd_remainder_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_terminal. fs_u_pfc_gcd_remainder_executionproductcoefficientsum = fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_remainder_executionproduct))) * fs_v_pfc_gcd_remainder_executionproductcoefficientsum) + (pfc_natural_sum_gcd_remainder_executionproductcoefficient))) /\ forall fs_i_pfc_gcd_remainder_executionproductcoefficientsum_body_steps. (exists fs_lt_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_bound. fs_lt_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_bound + S fs_i_pfc_gcd_remainder_executionproductcoefficientsum_body_steps = S (pfc_index_gcd_remainder_executionproduct)) -> exists fs_a_pfc_gcd_remainder_executionproductcoefficientsum_body_steps fs_r_pfc_gcd_remainder_executionproductcoefficientsum_body_steps fs_s_pfc_gcd_remainder_executionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_summand. fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_remainder_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_remainder_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_gcd_remainder_executionproductcoefficient)) /\ exists fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_summand. pfc_terms_code_gcd_remainder_executionproductcoefficient = fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_remainder_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_gcd_remainder_executionproductcoefficient) + (fs_a_pfc_gcd_remainder_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_partial. fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_remainder_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_remainder_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_remainder_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_partial. fs_u_pfc_gcd_remainder_executionproductcoefficientsum = fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_remainder_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_remainder_executionproductcoefficientsum) + (fs_r_pfc_gcd_remainder_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_successor. fs_h_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_remainder_executionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_remainder_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_remainder_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_successor. fs_u_pfc_gcd_remainder_executionproductcoefficientsum = fs_q_pfc_gcd_remainder_executionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_remainder_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_remainder_executionproductcoefficientsum) + (fs_s_pfc_gcd_remainder_executionproductcoefficientsum_body_steps))) /\ fs_s_pfc_gcd_remainder_executionproductcoefficientsum_body_steps = fs_r_pfc_gcd_remainder_executionproductcoefficientsum_body_steps + fs_a_pfc_gcd_remainder_executionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_remainder_executionproductcoefficientresiduebound. pfa_gap_gcd_remainder_executionproductcoefficientresiduebound + S (pfc_value_gcd_remainder_executionproduct) = (p)) /\ ((exists pfa_offset_left_gcd_remainder_executionproductcoefficientresiduecongruence pfa_offset_right_gcd_remainder_executionproductcoefficientresiduecongruence. (pfc_natural_sum_gcd_remainder_executionproductcoefficient) + (p) * pfa_offset_left_gcd_remainder_executionproductcoefficientresiduecongruence = (pfc_value_gcd_remainder_executionproduct) + (p) * pfa_offset_right_gcd_remainder_executionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_gcd_remainder_executiondifference. (exists pfa_gap_gcd_remainder_executiondifferenceindex. pfa_gap_gcd_remainder_executiondifferenceindex + S (pfs_index_gcd_remainder_executiondifference) = (L)) -> exists pfs_left_gcd_remainder_executiondifference pfs_right_gcd_remainder_executiondifference pfs_result_gcd_remainder_executiondifference. ((((exists ff_h_pfp_gcd_remainder_executiondifferenceleft. ff_h_pfp_gcd_remainder_executiondifferenceleft + S (pfs_left_gcd_remainder_executiondifference) = S ((S (pfs_index_gcd_remainder_executiondifference)) * ac)) /\ exists ff_q_pfp_gcd_remainder_executiondifferenceleft. ab = ff_q_pfp_gcd_remainder_executiondifferenceleft * S ((S (pfs_index_gcd_remainder_executiondifference)) * ac) + (pfs_left_gcd_remainder_executiondifference))) /\ (((((exists ff_h_pfp_gcd_remainder_executiondifferenceright. ff_h_pfp_gcd_remainder_executiondifferenceright + S (pfs_right_gcd_remainder_executiondifference) = S ((S (pfs_index_gcd_remainder_executiondifference)) * pfd_product_scale_gcd_remainder_execution)) /\ exists ff_q_pfp_gcd_remainder_executiondifferenceright. pfd_product_code_gcd_remainder_execution = ff_q_pfp_gcd_remainder_executiondifferenceright * S ((S (pfs_index_gcd_remainder_executiondifference)) * pfd_product_scale_gcd_remainder_execution) + (pfs_right_gcd_remainder_executiondifference))) /\ (((((exists ff_h_pfp_gcd_remainder_executiondifferenceresult. ff_h_pfp_gcd_remainder_executiondifferenceresult + S (pfs_result_gcd_remainder_executiondifference) = S ((S (pfs_index_gcd_remainder_executiondifference)) * pfd_residual_scale_gcd_remainder_execution)) /\ exists ff_q_pfp_gcd_remainder_executiondifferenceresult. pfd_residual_code_gcd_remainder_execution = ff_q_pfp_gcd_remainder_executiondifferenceresult * S ((S (pfs_index_gcd_remainder_executiondifference)) * pfd_residual_scale_gcd_remainder_execution) + (pfs_result_gcd_remainder_executiondifference))) /\ ((((exists pfa_gap_gcd_remainder_executiondifferenceoperationleft. pfa_gap_gcd_remainder_executiondifferenceoperationleft + S (pfs_right_gcd_remainder_executiondifference) = (p)) /\ (((exists pfa_gap_gcd_remainder_executiondifferenceoperationright. pfa_gap_gcd_remainder_executiondifferenceoperationright + S (pfs_result_gcd_remainder_executiondifference) = (p)) /\ ((((exists pfa_gap_gcd_remainder_executiondifferenceoperationresultbound. pfa_gap_gcd_remainder_executiondifferenceoperationresultbound + S (pfs_left_gcd_remainder_executiondifference) = (p)) /\ ((exists pfa_offset_left_gcd_remainder_executiondifferenceoperationresultcongruence pfa_offset_right_gcd_remainder_executiondifferenceoperationresultcongruence. ((pfs_right_gcd_remainder_executiondifference) + (pfs_result_gcd_remainder_executiondifference)) + (p) * pfa_offset_left_gcd_remainder_executiondifferenceoperationresultcongruence = (pfs_left_gcd_remainder_executiondifference) + (p) * pfa_offset_right_gcd_remainder_executiondifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_gcd_remainder_execution)+(R)) /\ (((forall fom_index_pfp_gcd_remainder_executiontriminput. (exists fom_gap_pfp_gcd_remainder_executiontriminput_index_bound. fom_gap_pfp_gcd_remainder_executiontriminput_index_bound + S (fom_index_pfp_gcd_remainder_executiontriminput) = L) -> exists fom_value_pfp_gcd_remainder_executiontriminput. ((((exists fom_beta_height_pfp_gcd_remainder_executiontriminput_entry. fom_beta_height_pfp_gcd_remainder_executiontriminput_entry + S (fom_value_pfp_gcd_remainder_executiontriminput) = S ((S (fom_index_pfp_gcd_remainder_executiontriminput)) * pfd_residual_scale_gcd_remainder_execution)) /\ exists fom_beta_quotient_pfp_gcd_remainder_executiontriminput_entry. pfd_residual_code_gcd_remainder_execution = fom_beta_quotient_pfp_gcd_remainder_executiontriminput_entry * S ((S (fom_index_pfp_gcd_remainder_executiontriminput)) * pfd_residual_scale_gcd_remainder_execution) + (fom_value_pfp_gcd_remainder_executiontriminput))) /\ (exists fom_gap_pfp_gcd_remainder_executiontriminput_value_bound. fom_gap_pfp_gcd_remainder_executiontriminput_value_bound + S (fom_value_pfp_gcd_remainder_executiontriminput) = p))) /\ (((forall pfp_repeat_index_gcd_remainder_executiontrimremoved. (exists pfa_gap_gcd_remainder_executiontrimremovedindex. pfa_gap_gcd_remainder_executiontrimremovedindex + S (pfp_repeat_index_gcd_remainder_executiontrimremoved) = (pfd_cut_gcd_remainder_execution)) -> (((exists ff_h_pfp_gcd_remainder_executiontrimremovedentry. ff_h_pfp_gcd_remainder_executiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_gcd_remainder_executiontrimremoved)) * pfd_residual_scale_gcd_remainder_execution)) /\ exists ff_q_pfp_gcd_remainder_executiontrimremovedentry. pfd_residual_code_gcd_remainder_execution = ff_q_pfp_gcd_remainder_executiontrimremovedentry * S ((S (pfp_repeat_index_gcd_remainder_executiontrimremoved)) * pfd_residual_scale_gcd_remainder_execution) + (0)))) /\ (((forall pftrim_index_gcd_remainder_executiontrimsuffix pftrim_value_gcd_remainder_executiontrimsuffix. (exists pfa_gap_gcd_remainder_executiontrimsuffixbound. pfa_gap_gcd_remainder_executiontrimsuffixbound + S (pftrim_index_gcd_remainder_executiontrimsuffix) = (R)) -> (((exists ff_h_pfp_gcd_remainder_executiontrimsuffixsource. ff_h_pfp_gcd_remainder_executiontrimsuffixsource + S (pftrim_value_gcd_remainder_executiontrimsuffix) = S ((S ((pfd_cut_gcd_remainder_execution)+pftrim_index_gcd_remainder_executiontrimsuffix)) * pfd_residual_scale_gcd_remainder_execution)) /\ exists ff_q_pfp_gcd_remainder_executiontrimsuffixsource. pfd_residual_code_gcd_remainder_execution = ff_q_pfp_gcd_remainder_executiontrimsuffixsource * S ((S ((pfd_cut_gcd_remainder_execution)+pftrim_index_gcd_remainder_executiontrimsuffix)) * pfd_residual_scale_gcd_remainder_execution) + (pftrim_value_gcd_remainder_executiontrimsuffix))) -> (((exists ff_h_pfp_gcd_remainder_executiontrimsuffixoutput. ff_h_pfp_gcd_remainder_executiontrimsuffixoutput + S (pftrim_value_gcd_remainder_executiontrimsuffix) = S ((S (pftrim_index_gcd_remainder_executiontrimsuffix)) * rc)) /\ exists ff_q_pfp_gcd_remainder_executiontrimsuffixoutput. rb = ff_q_pfp_gcd_remainder_executiontrimsuffixoutput * S ((S (pftrim_index_gcd_remainder_executiontrimsuffix)) * rc) + (pftrim_value_gcd_remainder_executiontrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_gcd_remainder_executiontrimnormal. ((((exists ff_h_pfp_gcd_remainder_executiontrimnormalentry. ff_h_pfp_gcd_remainder_executiontrimnormalentry + S (pftrim_leading_gcd_remainder_executiontrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_gcd_remainder_executiontrimnormalentry. rb = ff_q_pfp_gcd_remainder_executiontrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_gcd_remainder_executiontrimnormal))) /\ ((~(pftrim_leading_gcd_remainder_executiontrimnormal=0))))))))))))))))))))))))))))))))) -> (forall fom_index_pfp_gcd_remainder_bounded. (exists fom_gap_pfp_gcd_remainder_bounded_index_bound. fom_gap_pfp_gcd_remainder_bounded_index_bound + S (fom_index_pfp_gcd_remainder_bounded) = R) -> exists fom_value_pfp_gcd_remainder_bounded. ((((exists fom_beta_height_pfp_gcd_remainder_bounded_entry. fom_beta_height_pfp_gcd_remainder_bounded_entry + S (fom_value_pfp_gcd_remainder_bounded) = S ((S (fom_index_pfp_gcd_remainder_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_gcd_remainder_bounded_entry. rb = fom_beta_quotient_pfp_gcd_remainder_bounded_entry * S ((S (fom_index_pfp_gcd_remainder_bounded)) * rc) + (fom_value_pfp_gcd_remainder_bounded))) /\ (exists fom_gap_pfp_gcd_remainder_bounded_value_bound. fom_gap_pfp_gcd_remainder_bounded_value_bound + S (fom_value_pfp_gcd_remainder_bounded) = p)))