prime_field_polynomial_gcd_bezout_division_backward

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_gcd_backward_prime pfa_factor_right_gcd_backward_prime. (p) = pfa_factor_left_gcd_backward_prime * pfa_factor_right_gcd_backward_prime -> pfa_factor_left_gcd_backward_prime = 1 \/ pfa_factor_right_gcd_backward_prime = 1) -> (((forall fom_index_pfp_gcd_backward_executioninput. (exists fom_gap_pfp_gcd_backward_executioninput_index_bound. fom_gap_pfp_gcd_backward_executioninput_index_bound + S (fom_index_pfp_gcd_backward_executioninput) = L) -> exists fom_value_pfp_gcd_backward_executioninput. ((((exists fom_beta_height_pfp_gcd_backward_executioninput_entry. fom_beta_height_pfp_gcd_backward_executioninput_entry + S (fom_value_pfp_gcd_backward_executioninput) = S ((S (fom_index_pfp_gcd_backward_executioninput)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_backward_executioninput_entry. ab = fom_beta_quotient_pfp_gcd_backward_executioninput_entry * S ((S (fom_index_pfp_gcd_backward_executioninput)) * ac) + (fom_value_pfp_gcd_backward_executioninput))) /\ (exists fom_gap_pfp_gcd_backward_executioninput_value_bound. fom_gap_pfp_gcd_backward_executioninput_value_bound + S (fom_value_pfp_gcd_backward_executioninput) = p))) /\ (((forall fom_index_pfp_gcd_backward_executiondivisor. (exists fom_gap_pfp_gcd_backward_executiondivisor_index_bound. fom_gap_pfp_gcd_backward_executiondivisor_index_bound + S (fom_index_pfp_gcd_backward_executiondivisor) = S (d)) -> exists fom_value_pfp_gcd_backward_executiondivisor. ((((exists fom_beta_height_pfp_gcd_backward_executiondivisor_entry. fom_beta_height_pfp_gcd_backward_executiondivisor_entry + S (fom_value_pfp_gcd_backward_executiondivisor) = S ((S (fom_index_pfp_gcd_backward_executiondivisor)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_executiondivisor_entry. bb = fom_beta_quotient_pfp_gcd_backward_executiondivisor_entry * S ((S (fom_index_pfp_gcd_backward_executiondivisor)) * bc) + (fom_value_pfp_gcd_backward_executiondivisor))) /\ (exists fom_gap_pfp_gcd_backward_executiondivisor_value_bound. fom_gap_pfp_gcd_backward_executiondivisor_value_bound + S (fom_value_pfp_gcd_backward_executiondivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_gcd_backward_executionlengthshort. pfc_gap_gcd_backward_executionlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_gcd_backward_execution pfd_inverse_gcd_backward_execution pfd_product_code_gcd_backward_execution pfd_product_scale_gcd_backward_execution pfd_residual_code_gcd_backward_execution pfd_residual_scale_gcd_backward_execution pfd_cut_gcd_backward_execution. ((((exists ff_h_pfp_gcd_backward_executionhead. ff_h_pfp_gcd_backward_executionhead + S (pfd_head_gcd_backward_execution) = S ((S (0)) * bc)) /\ exists ff_q_pfp_gcd_backward_executionhead. bb = ff_q_pfp_gcd_backward_executionhead * S ((S (0)) * bc) + (pfd_head_gcd_backward_execution))) /\ (((((~((pfd_head_gcd_backward_execution) = 0)) /\ ((((exists pfa_gap_gcd_backward_executioninversemultiplicationleft. pfa_gap_gcd_backward_executioninversemultiplicationleft + S (pfd_head_gcd_backward_execution) = (p)) /\ (((exists pfa_gap_gcd_backward_executioninversemultiplicationright. pfa_gap_gcd_backward_executioninversemultiplicationright + S (pfd_inverse_gcd_backward_execution) = (p)) /\ ((((exists pfa_gap_gcd_backward_executioninversemultiplicationresultbound. pfa_gap_gcd_backward_executioninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executioninversemultiplicationresultcongruence pfa_offset_right_gcd_backward_executioninversemultiplicationresultcongruence. ((pfd_head_gcd_backward_execution) * (pfd_inverse_gcd_backward_execution)) + (p) * pfa_offset_left_gcd_backward_executioninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_gcd_backward_executioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_gcd_backward_executionquotient. (exists pfa_gap_gcd_backward_executionquotientbound. pfa_gap_gcd_backward_executionquotientbound + S (pfd_index_gcd_backward_executionquotient) = (q)) -> exists pfd_value_gcd_backward_executionquotient. ((((exists ff_h_pfp_gcd_backward_executionquotiententry. ff_h_pfp_gcd_backward_executionquotiententry + S (pfd_value_gcd_backward_executionquotient) = S ((S (pfd_index_gcd_backward_executionquotient)) * qc)) /\ exists ff_q_pfp_gcd_backward_executionquotiententry. qb = ff_q_pfp_gcd_backward_executionquotiententry * S ((S (pfd_index_gcd_backward_executionquotient)) * qc) + (pfd_value_gcd_backward_executionquotient))) /\ ((exists pfd_input_gcd_backward_executionquotientstep pfd_previous_gcd_backward_executionquotientstep pfd_difference_gcd_backward_executionquotientstep. ((((exists ff_h_pfp_gcd_backward_executionquotientstepinput. ff_h_pfp_gcd_backward_executionquotientstepinput + S (pfd_input_gcd_backward_executionquotientstep) = S ((S (pfd_index_gcd_backward_executionquotient)) * ac)) /\ exists ff_q_pfp_gcd_backward_executionquotientstepinput. ab = ff_q_pfp_gcd_backward_executionquotientstepinput * S ((S (pfd_index_gcd_backward_executionquotient)) * ac) + (pfd_input_gcd_backward_executionquotientstep))) /\ (((exists pfc_terms_code_gcd_backward_executionquotientstepprevious pfc_terms_scale_gcd_backward_executionquotientstepprevious pfc_natural_sum_gcd_backward_executionquotientstepprevious. ((forall pfc_index_gcd_backward_executionquotientsteppreviousdiagonal. (exists pfa_gap_gcd_backward_executionquotientsteppreviousdiagonalbound. pfa_gap_gcd_backward_executionquotientsteppreviousdiagonalbound + S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal) = (S (pfd_index_gcd_backward_executionquotient))) -> exists pfc_value_gcd_backward_executionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonalentry. ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonalentry + S (pfc_value_gcd_backward_executionquotientsteppreviousdiagonal) = S ((S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_gcd_backward_executionquotientstepprevious)) /\ exists ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonalentry. pfc_terms_code_gcd_backward_executionquotientstepprevious = ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonalentry * S ((S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_gcd_backward_executionquotientstepprevious) + (pfc_value_gcd_backward_executionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm. (((pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)+pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm=(pfd_index_gcd_backward_executionquotient)) /\ ((((((exists pfa_gap_gcd_backward_executionquotientsteppreviousdiagonaltermleftinside. pfa_gap_gcd_backward_executionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal) = (pfd_index_gcd_backward_executionquotient)) /\ ((((exists ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) * qc) + (pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_executionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_gcd_backward_executionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_gcd_backward_executionquotient)=(pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) /\ (((pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_executionquotientsteppreviousdiagonaltermrightinside. pfa_gap_gcd_backward_executionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_executionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_gcd_backward_executionquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_executionquotientsteppreviousdiagonal)=pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm*pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_executionquotientstepprevioussum fs_v_pfc_gcd_backward_executionquotientstepprevioussum. ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_start. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_start. fs_u_pfc_gcd_backward_executionquotientstepprevioussum = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_terminal. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_gcd_backward_executionquotientstepprevious) = S ((S (S (pfd_index_gcd_backward_executionquotient))) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_terminal. fs_u_pfc_gcd_backward_executionquotientstepprevioussum = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_gcd_backward_executionquotient))) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum) + (pfc_natural_sum_gcd_backward_executionquotientstepprevious))) /\ forall fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps = S (pfd_index_gcd_backward_executionquotient)) -> exists fs_a_pfc_gcd_backward_executionquotientstepprevioussum_body_steps fs_r_pfc_gcd_backward_executionquotientstepprevioussum_body_steps fs_s_pfc_gcd_backward_executionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_summand. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_gcd_backward_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_gcd_backward_executionquotientstepprevious)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_summand. pfc_terms_code_gcd_backward_executionquotientstepprevious = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_gcd_backward_executionquotientstepprevious) + (fs_a_pfc_gcd_backward_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_partial. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_gcd_backward_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_partial. fs_u_pfc_gcd_backward_executionquotientstepprevioussum = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum) + (fs_r_pfc_gcd_backward_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_successor. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_gcd_backward_executionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_successor. fs_u_pfc_gcd_backward_executionquotientstepprevioussum = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum) + (fs_s_pfc_gcd_backward_executionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_gcd_backward_executionquotientstepprevioussum_body_steps = fs_r_pfc_gcd_backward_executionquotientstepprevioussum_body_steps + fs_a_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_executionquotientsteppreviousresiduebound. pfa_gap_gcd_backward_executionquotientsteppreviousresiduebound + S (pfd_previous_gcd_backward_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executionquotientsteppreviousresiduecongruence pfa_offset_right_gcd_backward_executionquotientsteppreviousresiduecongruence. (pfc_natural_sum_gcd_backward_executionquotientstepprevious) + (p) * pfa_offset_left_gcd_backward_executionquotientsteppreviousresiduecongruence = (pfd_previous_gcd_backward_executionquotientstep) + (p) * pfa_offset_right_gcd_backward_executionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_gcd_backward_executionquotientstepsubtractleft. pfa_gap_gcd_backward_executionquotientstepsubtractleft + S (pfd_previous_gcd_backward_executionquotientstep) = (p)) /\ (((exists pfa_gap_gcd_backward_executionquotientstepsubtractright. pfa_gap_gcd_backward_executionquotientstepsubtractright + S (pfd_difference_gcd_backward_executionquotientstep) = (p)) /\ ((((exists pfa_gap_gcd_backward_executionquotientstepsubtractresultbound. pfa_gap_gcd_backward_executionquotientstepsubtractresultbound + S (pfd_input_gcd_backward_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executionquotientstepsubtractresultcongruence pfa_offset_right_gcd_backward_executionquotientstepsubtractresultcongruence. ((pfd_previous_gcd_backward_executionquotientstep) + (pfd_difference_gcd_backward_executionquotientstep)) + (p) * pfa_offset_left_gcd_backward_executionquotientstepsubtractresultcongruence = (pfd_input_gcd_backward_executionquotientstep) + (p) * pfa_offset_right_gcd_backward_executionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_gcd_backward_executionquotientstepmultiplyleft. pfa_gap_gcd_backward_executionquotientstepmultiplyleft + S (pfd_inverse_gcd_backward_execution) = (p)) /\ (((exists pfa_gap_gcd_backward_executionquotientstepmultiplyright. pfa_gap_gcd_backward_executionquotientstepmultiplyright + S (pfd_difference_gcd_backward_executionquotientstep) = (p)) /\ ((((exists pfa_gap_gcd_backward_executionquotientstepmultiplyresultbound. pfa_gap_gcd_backward_executionquotientstepmultiplyresultbound + S (pfd_value_gcd_backward_executionquotient) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executionquotientstepmultiplyresultcongruence pfa_offset_right_gcd_backward_executionquotientstepmultiplyresultcongruence. ((pfd_inverse_gcd_backward_execution) * (pfd_difference_gcd_backward_executionquotientstep)) + (p) * pfa_offset_left_gcd_backward_executionquotientstepmultiplyresultcongruence = (pfd_value_gcd_backward_executionquotient) + (p) * pfa_offset_right_gcd_backward_executionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_gcd_backward_executionproduct. (exists pfa_gap_gcd_backward_executionproductbound. pfa_gap_gcd_backward_executionproductbound + S (pfc_index_gcd_backward_executionproduct) = (L)) -> exists pfc_value_gcd_backward_executionproduct. ((((exists ff_h_pfp_gcd_backward_executionproductentry. ff_h_pfp_gcd_backward_executionproductentry + S (pfc_value_gcd_backward_executionproduct) = S ((S (pfc_index_gcd_backward_executionproduct)) * pfd_product_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executionproductentry. pfd_product_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executionproductentry * S ((S (pfc_index_gcd_backward_executionproduct)) * pfd_product_scale_gcd_backward_execution) + (pfc_value_gcd_backward_executionproduct))) /\ ((exists pfc_terms_code_gcd_backward_executionproductcoefficient pfc_terms_scale_gcd_backward_executionproductcoefficient pfc_natural_sum_gcd_backward_executionproductcoefficient. ((forall pfc_index_gcd_backward_executionproductcoefficientdiagonal. (exists pfa_gap_gcd_backward_executionproductcoefficientdiagonalbound. pfa_gap_gcd_backward_executionproductcoefficientdiagonalbound + S (pfc_index_gcd_backward_executionproductcoefficientdiagonal) = (S (pfc_index_gcd_backward_executionproduct))) -> exists pfc_value_gcd_backward_executionproductcoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_executionproductcoefficientdiagonalentry. ff_h_pfp_gcd_backward_executionproductcoefficientdiagonalentry + S (pfc_value_gcd_backward_executionproductcoefficientdiagonal) = S ((S (pfc_index_gcd_backward_executionproductcoefficientdiagonal)) * pfc_terms_scale_gcd_backward_executionproductcoefficient)) /\ exists ff_q_pfp_gcd_backward_executionproductcoefficientdiagonalentry. pfc_terms_code_gcd_backward_executionproductcoefficient = ff_q_pfp_gcd_backward_executionproductcoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_executionproductcoefficientdiagonal)) * pfc_terms_scale_gcd_backward_executionproductcoefficient) + (pfc_value_gcd_backward_executionproductcoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm pfc_left_gcd_backward_executionproductcoefficientdiagonalterm pfc_right_gcd_backward_executionproductcoefficientdiagonalterm. (((pfc_index_gcd_backward_executionproductcoefficientdiagonal)+pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm=(pfc_index_gcd_backward_executionproduct)) /\ ((((((exists pfa_gap_gcd_backward_executionproductcoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_executionproductcoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_executionproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_gcd_backward_executionproductcoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_executionproductcoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_executionproductcoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_executionproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_gcd_backward_executionproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_gcd_backward_executionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_executionproductcoefficientdiagonal)) * qc) + (pfc_left_gcd_backward_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_executionproductcoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_executionproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_gcd_backward_executionproductcoefficientdiagonal)) /\ (((pfc_left_gcd_backward_executionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_executionproductcoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_executionproductcoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_gcd_backward_executionproductcoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_executionproductcoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_executionproductcoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_backward_executionproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_backward_executionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm)) * bc) + (pfc_right_gcd_backward_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_executionproductcoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_executionproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_executionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_executionproductcoefficientdiagonal)=pfc_left_gcd_backward_executionproductcoefficientdiagonalterm*pfc_right_gcd_backward_executionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_executionproductcoefficientsum fs_v_pfc_gcd_backward_executionproductcoefficientsum. ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_start. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_start. fs_u_pfc_gcd_backward_executionproductcoefficientsum = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_terminal. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_executionproductcoefficient) = S ((S (S (pfc_index_gcd_backward_executionproduct))) * fs_v_pfc_gcd_backward_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_terminal. fs_u_pfc_gcd_backward_executionproductcoefficientsum = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_executionproduct))) * fs_v_pfc_gcd_backward_executionproductcoefficientsum) + (pfc_natural_sum_gcd_backward_executionproductcoefficient))) /\ forall fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_executionproductcoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_executionproductcoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps = S (pfc_index_gcd_backward_executionproduct)) -> exists fs_a_pfc_gcd_backward_executionproductcoefficientsum_body_steps fs_r_pfc_gcd_backward_executionproductcoefficientsum_body_steps fs_s_pfc_gcd_backward_executionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_executionproductcoefficient)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_executionproductcoefficient = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_executionproductcoefficient) + (fs_a_pfc_gcd_backward_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_executionproductcoefficientsum = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum) + (fs_r_pfc_gcd_backward_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_executionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_executionproductcoefficientsum = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum) + (fs_s_pfc_gcd_backward_executionproductcoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_executionproductcoefficientsum_body_steps = fs_r_pfc_gcd_backward_executionproductcoefficientsum_body_steps + fs_a_pfc_gcd_backward_executionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_executionproductcoefficientresiduebound. pfa_gap_gcd_backward_executionproductcoefficientresiduebound + S (pfc_value_gcd_backward_executionproduct) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executionproductcoefficientresiduecongruence pfa_offset_right_gcd_backward_executionproductcoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_executionproductcoefficient) + (p) * pfa_offset_left_gcd_backward_executionproductcoefficientresiduecongruence = (pfc_value_gcd_backward_executionproduct) + (p) * pfa_offset_right_gcd_backward_executionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_gcd_backward_executiondifference. (exists pfa_gap_gcd_backward_executiondifferenceindex. pfa_gap_gcd_backward_executiondifferenceindex + S (pfs_index_gcd_backward_executiondifference) = (L)) -> exists pfs_left_gcd_backward_executiondifference pfs_right_gcd_backward_executiondifference pfs_result_gcd_backward_executiondifference. ((((exists ff_h_pfp_gcd_backward_executiondifferenceleft. ff_h_pfp_gcd_backward_executiondifferenceleft + S (pfs_left_gcd_backward_executiondifference) = S ((S (pfs_index_gcd_backward_executiondifference)) * ac)) /\ exists ff_q_pfp_gcd_backward_executiondifferenceleft. ab = ff_q_pfp_gcd_backward_executiondifferenceleft * S ((S (pfs_index_gcd_backward_executiondifference)) * ac) + (pfs_left_gcd_backward_executiondifference))) /\ (((((exists ff_h_pfp_gcd_backward_executiondifferenceright. ff_h_pfp_gcd_backward_executiondifferenceright + S (pfs_right_gcd_backward_executiondifference) = S ((S (pfs_index_gcd_backward_executiondifference)) * pfd_product_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executiondifferenceright. pfd_product_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executiondifferenceright * S ((S (pfs_index_gcd_backward_executiondifference)) * pfd_product_scale_gcd_backward_execution) + (pfs_right_gcd_backward_executiondifference))) /\ (((((exists ff_h_pfp_gcd_backward_executiondifferenceresult. ff_h_pfp_gcd_backward_executiondifferenceresult + S (pfs_result_gcd_backward_executiondifference) = S ((S (pfs_index_gcd_backward_executiondifference)) * pfd_residual_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executiondifferenceresult. pfd_residual_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executiondifferenceresult * S ((S (pfs_index_gcd_backward_executiondifference)) * pfd_residual_scale_gcd_backward_execution) + (pfs_result_gcd_backward_executiondifference))) /\ ((((exists pfa_gap_gcd_backward_executiondifferenceoperationleft. pfa_gap_gcd_backward_executiondifferenceoperationleft + S (pfs_right_gcd_backward_executiondifference) = (p)) /\ (((exists pfa_gap_gcd_backward_executiondifferenceoperationright. pfa_gap_gcd_backward_executiondifferenceoperationright + S (pfs_result_gcd_backward_executiondifference) = (p)) /\ ((((exists pfa_gap_gcd_backward_executiondifferenceoperationresultbound. pfa_gap_gcd_backward_executiondifferenceoperationresultbound + S (pfs_left_gcd_backward_executiondifference) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executiondifferenceoperationresultcongruence pfa_offset_right_gcd_backward_executiondifferenceoperationresultcongruence. ((pfs_right_gcd_backward_executiondifference) + (pfs_result_gcd_backward_executiondifference)) + (p) * pfa_offset_left_gcd_backward_executiondifferenceoperationresultcongruence = (pfs_left_gcd_backward_executiondifference) + (p) * pfa_offset_right_gcd_backward_executiondifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_gcd_backward_execution)+(R)) /\ (((forall fom_index_pfp_gcd_backward_executiontriminput. (exists fom_gap_pfp_gcd_backward_executiontriminput_index_bound. fom_gap_pfp_gcd_backward_executiontriminput_index_bound + S (fom_index_pfp_gcd_backward_executiontriminput) = L) -> exists fom_value_pfp_gcd_backward_executiontriminput. ((((exists fom_beta_height_pfp_gcd_backward_executiontriminput_entry. fom_beta_height_pfp_gcd_backward_executiontriminput_entry + S (fom_value_pfp_gcd_backward_executiontriminput) = S ((S (fom_index_pfp_gcd_backward_executiontriminput)) * pfd_residual_scale_gcd_backward_execution)) /\ exists fom_beta_quotient_pfp_gcd_backward_executiontriminput_entry. pfd_residual_code_gcd_backward_execution = fom_beta_quotient_pfp_gcd_backward_executiontriminput_entry * S ((S (fom_index_pfp_gcd_backward_executiontriminput)) * pfd_residual_scale_gcd_backward_execution) + (fom_value_pfp_gcd_backward_executiontriminput))) /\ (exists fom_gap_pfp_gcd_backward_executiontriminput_value_bound. fom_gap_pfp_gcd_backward_executiontriminput_value_bound + S (fom_value_pfp_gcd_backward_executiontriminput) = p))) /\ (((forall pfp_repeat_index_gcd_backward_executiontrimremoved. (exists pfa_gap_gcd_backward_executiontrimremovedindex. pfa_gap_gcd_backward_executiontrimremovedindex + S (pfp_repeat_index_gcd_backward_executiontrimremoved) = (pfd_cut_gcd_backward_execution)) -> (((exists ff_h_pfp_gcd_backward_executiontrimremovedentry. ff_h_pfp_gcd_backward_executiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_gcd_backward_executiontrimremoved)) * pfd_residual_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executiontrimremovedentry. pfd_residual_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executiontrimremovedentry * S ((S (pfp_repeat_index_gcd_backward_executiontrimremoved)) * pfd_residual_scale_gcd_backward_execution) + (0)))) /\ (((forall pftrim_index_gcd_backward_executiontrimsuffix pftrim_value_gcd_backward_executiontrimsuffix. (exists pfa_gap_gcd_backward_executiontrimsuffixbound. pfa_gap_gcd_backward_executiontrimsuffixbound + S (pftrim_index_gcd_backward_executiontrimsuffix) = (R)) -> (((exists ff_h_pfp_gcd_backward_executiontrimsuffixsource. ff_h_pfp_gcd_backward_executiontrimsuffixsource + S (pftrim_value_gcd_backward_executiontrimsuffix) = S ((S ((pfd_cut_gcd_backward_execution)+pftrim_index_gcd_backward_executiontrimsuffix)) * pfd_residual_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executiontrimsuffixsource. pfd_residual_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executiontrimsuffixsource * S ((S ((pfd_cut_gcd_backward_execution)+pftrim_index_gcd_backward_executiontrimsuffix)) * pfd_residual_scale_gcd_backward_execution) + (pftrim_value_gcd_backward_executiontrimsuffix))) -> (((exists ff_h_pfp_gcd_backward_executiontrimsuffixoutput. ff_h_pfp_gcd_backward_executiontrimsuffixoutput + S (pftrim_value_gcd_backward_executiontrimsuffix) = S ((S (pftrim_index_gcd_backward_executiontrimsuffix)) * rc)) /\ exists ff_q_pfp_gcd_backward_executiontrimsuffixoutput. rb = ff_q_pfp_gcd_backward_executiontrimsuffixoutput * S ((S (pftrim_index_gcd_backward_executiontrimsuffix)) * rc) + (pftrim_value_gcd_backward_executiontrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_gcd_backward_executiontrimnormal. ((((exists ff_h_pfp_gcd_backward_executiontrimnormalentry. ff_h_pfp_gcd_backward_executiontrimnormalentry + S (pftrim_leading_gcd_backward_executiontrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_gcd_backward_executiontrimnormalentry. rb = ff_q_pfp_gcd_backward_executiontrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_gcd_backward_executiontrimnormal))) /\ ((~(pftrim_leading_gcd_backward_executiontrimnormal=0))))))))))))))))))))))))))))))))) -> (exists pfgs_gb_gcd_backward_small pfgs_gc_gcd_backward_small pfgs_G_gcd_backward_small pfgs_ub_gcd_backward_small pfgs_uc_gcd_backward_small pfgs_U_gcd_backward_small pfgs_vb_gcd_backward_small pfgs_vc_gcd_backward_small pfgs_V_gcd_backward_small. (((pfgs_G_gcd_backward_small)=0 \/ (((~((pfgs_G_gcd_backward_small) = 0)) /\ (((forall fom_index_pfp_gcd_backward_small_witness_normal_moniccoefficients. (exists fom_gap_pfp_gcd_backward_small_witness_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_backward_small_witness_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_backward_small_witness_normal_moniccoefficients) = pfgs_G_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_backward_small_witness_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_backward_small_witness_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_backward_small_witness_normal_moniccoefficients)) * pfgs_gc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_normal_moniccoefficients_entry. pfgs_gb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_normal_moniccoefficients)) * pfgs_gc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_backward_small_witness_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_backward_small_witness_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_normal_monicleading. ff_h_pfp_gcd_backward_small_witness_normal_monicleading + S (1) = S ((S (0)) * pfgs_gc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_normal_monicleading. pfgs_gb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_normal_monicleading * S ((S (0)) * pfgs_gc_gcd_backward_small) + (1))))))))) /\ (((((((forall fom_index_pfp_gcd_backward_small_witness_common_left_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_common_left_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_left_bounded) = S d) -> exists fom_value_pfp_gcd_backward_small_witness_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_left_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_left_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_common_left_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_bounded_entry. bb = fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_bounded)) * bc) + (fom_value_pfp_gcd_backward_small_witness_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_left_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_backward_small_witness_common_left pfgd_qc_gcd_backward_small_witness_common_left pfgd_Q_gcd_backward_small_witness_common_left pfgd_pb_gcd_backward_small_witness_common_left pfgd_pc_gcd_backward_small_witness_common_left pfgd_P_gcd_backward_small_witness_common_left. ((((forall fom_index_pfp_gcd_backward_small_witness_common_left_productleft. (exists fom_gap_pfp_gcd_backward_small_witness_common_left_productleft_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_productleft_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_left_productleft) = pfgd_Q_gcd_backward_small_witness_common_left) -> exists fom_value_pfp_gcd_backward_small_witness_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_left_productleft_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_left_productleft_entry + S (fom_value_pfp_gcd_backward_small_witness_common_left_productleft) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_productleft)) * pfgd_qc_gcd_backward_small_witness_common_left)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_productleft_entry. pfgd_qb_gcd_backward_small_witness_common_left = fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_productleft)) * pfgd_qc_gcd_backward_small_witness_common_left) + (fom_value_pfp_gcd_backward_small_witness_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_left_productleft_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_productleft_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_common_left_productright. (exists fom_gap_pfp_gcd_backward_small_witness_common_left_productright_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_productright_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_left_productright) = pfgs_G_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_common_left_productright. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_left_productright_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_left_productright_entry + S (fom_value_pfp_gcd_backward_small_witness_common_left_productright) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_productright)) * pfgs_gc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_productright_entry. pfgs_gb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_productright_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_productright)) * pfgs_gc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_common_left_productright))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_left_productright_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_productright_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_backward_small_witness_common_left)=0 \/ (pfgs_G_gcd_backward_small)=0) /\ (((pfgd_P_gcd_backward_small_witness_common_left)=0)))) \/ (((~((pfgd_Q_gcd_backward_small_witness_common_left)=0)) /\ (((~((pfgs_G_gcd_backward_small)=0)) /\ (((pfgd_Q_gcd_backward_small_witness_common_left)+(pfgs_G_gcd_backward_small)=S (pfgd_P_gcd_backward_small_witness_common_left)))))))) /\ ((forall pfc_index_gcd_backward_small_witness_common_left_productcoefficients. (exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientsbound. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientsbound + S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients) = (pfgd_P_gcd_backward_small_witness_common_left)) -> exists pfc_value_gcd_backward_small_witness_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientsentry. ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientsentry + S (pfc_value_gcd_backward_small_witness_common_left_productcoefficients) = S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients)) * pfgd_pc_gcd_backward_small_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientsentry. pfgd_pb_gcd_backward_small_witness_common_left = ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients)) * pfgd_pc_gcd_backward_small_witness_common_left) + (pfc_value_gcd_backward_small_witness_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_small_witness_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_backward_small_witness_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients))) -> exists pfc_value_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_small_witness_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient) + (pfc_value_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_small_witness_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_backward_small_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_small_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_backward_small_witness_common_left = ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_small_witness_common_left) + (pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_backward_small_witness_common_left)=(pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_small) + (pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_backward_small)=(pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_small_witness_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_small_witness_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_small_witness_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_small_witness_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_small_witness_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_small_witness_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_backward_small_witness_common_left_equivalent pfrep_left_gcd_backward_small_witness_common_left_equivalent pfrep_right_gcd_backward_small_witness_common_left_equivalent. ((exists pfrep_position_gcd_backward_small_witness_common_left_equivalentfirst. ((pfrep_position_gcd_backward_small_witness_common_left_equivalentfirst+S (pfrep_power_gcd_backward_small_witness_common_left_equivalent)=(pfgd_P_gcd_backward_small_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_equivalentfirstentry. ff_h_pfp_gcd_backward_small_witness_common_left_equivalentfirstentry + S (pfrep_left_gcd_backward_small_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_backward_small_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_backward_small_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_equivalentfirstentry. pfgd_pb_gcd_backward_small_witness_common_left = ff_q_pfp_gcd_backward_small_witness_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_backward_small_witness_common_left) + (pfrep_left_gcd_backward_small_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_common_left_equivalentfirstoutside. pfrep_gap_gcd_backward_small_witness_common_left_equivalentfirstoutside+(pfgd_P_gcd_backward_small_witness_common_left)=(pfrep_power_gcd_backward_small_witness_common_left_equivalent)) /\ (((pfrep_left_gcd_backward_small_witness_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_common_left_equivalentsecond. ((pfrep_position_gcd_backward_small_witness_common_left_equivalentsecond+S (pfrep_power_gcd_backward_small_witness_common_left_equivalent)=(S d)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_equivalentsecondentry. ff_h_pfp_gcd_backward_small_witness_common_left_equivalentsecondentry + S (pfrep_right_gcd_backward_small_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_backward_small_witness_common_left_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_equivalentsecondentry. bb = ff_q_pfp_gcd_backward_small_witness_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_common_left_equivalentsecond)) * bc) + (pfrep_right_gcd_backward_small_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_common_left_equivalentsecondoutside. pfrep_gap_gcd_backward_small_witness_common_left_equivalentsecondoutside+(S d)=(pfrep_power_gcd_backward_small_witness_common_left_equivalent)) /\ (((pfrep_right_gcd_backward_small_witness_common_left_equivalent)=0))))) -> pfrep_left_gcd_backward_small_witness_common_left_equivalent=pfrep_right_gcd_backward_small_witness_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_backward_small_witness_common_right_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_common_right_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_right_bounded) = R) -> exists fom_value_pfp_gcd_backward_small_witness_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_right_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_right_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_common_right_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_bounded_entry. rb = fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_bounded)) * rc) + (fom_value_pfp_gcd_backward_small_witness_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_right_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_backward_small_witness_common_right pfgd_qc_gcd_backward_small_witness_common_right pfgd_Q_gcd_backward_small_witness_common_right pfgd_pb_gcd_backward_small_witness_common_right pfgd_pc_gcd_backward_small_witness_common_right pfgd_P_gcd_backward_small_witness_common_right. ((((forall fom_index_pfp_gcd_backward_small_witness_common_right_productleft. (exists fom_gap_pfp_gcd_backward_small_witness_common_right_productleft_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_productleft_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_right_productleft) = pfgd_Q_gcd_backward_small_witness_common_right) -> exists fom_value_pfp_gcd_backward_small_witness_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_right_productleft_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_right_productleft_entry + S (fom_value_pfp_gcd_backward_small_witness_common_right_productleft) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_productleft)) * pfgd_qc_gcd_backward_small_witness_common_right)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_productleft_entry. pfgd_qb_gcd_backward_small_witness_common_right = fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_productleft)) * pfgd_qc_gcd_backward_small_witness_common_right) + (fom_value_pfp_gcd_backward_small_witness_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_right_productleft_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_productleft_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_common_right_productright. (exists fom_gap_pfp_gcd_backward_small_witness_common_right_productright_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_productright_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_right_productright) = pfgs_G_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_common_right_productright. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_right_productright_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_right_productright_entry + S (fom_value_pfp_gcd_backward_small_witness_common_right_productright) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_productright)) * pfgs_gc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_productright_entry. pfgs_gb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_productright_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_productright)) * pfgs_gc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_common_right_productright))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_right_productright_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_productright_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_backward_small_witness_common_right)=0 \/ (pfgs_G_gcd_backward_small)=0) /\ (((pfgd_P_gcd_backward_small_witness_common_right)=0)))) \/ (((~((pfgd_Q_gcd_backward_small_witness_common_right)=0)) /\ (((~((pfgs_G_gcd_backward_small)=0)) /\ (((pfgd_Q_gcd_backward_small_witness_common_right)+(pfgs_G_gcd_backward_small)=S (pfgd_P_gcd_backward_small_witness_common_right)))))))) /\ ((forall pfc_index_gcd_backward_small_witness_common_right_productcoefficients. (exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientsbound. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientsbound + S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients) = (pfgd_P_gcd_backward_small_witness_common_right)) -> exists pfc_value_gcd_backward_small_witness_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientsentry. ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientsentry + S (pfc_value_gcd_backward_small_witness_common_right_productcoefficients) = S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients)) * pfgd_pc_gcd_backward_small_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientsentry. pfgd_pb_gcd_backward_small_witness_common_right = ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients)) * pfgd_pc_gcd_backward_small_witness_common_right) + (pfc_value_gcd_backward_small_witness_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_small_witness_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_backward_small_witness_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients))) -> exists pfc_value_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_small_witness_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient) + (pfc_value_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_small_witness_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_backward_small_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_small_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_backward_small_witness_common_right = ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_small_witness_common_right) + (pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_backward_small_witness_common_right)=(pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_small) + (pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_backward_small)=(pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_small_witness_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_small_witness_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_small_witness_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_small_witness_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_small_witness_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_small_witness_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_backward_small_witness_common_right_equivalent pfrep_left_gcd_backward_small_witness_common_right_equivalent pfrep_right_gcd_backward_small_witness_common_right_equivalent. ((exists pfrep_position_gcd_backward_small_witness_common_right_equivalentfirst. ((pfrep_position_gcd_backward_small_witness_common_right_equivalentfirst+S (pfrep_power_gcd_backward_small_witness_common_right_equivalent)=(pfgd_P_gcd_backward_small_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_equivalentfirstentry. ff_h_pfp_gcd_backward_small_witness_common_right_equivalentfirstentry + S (pfrep_left_gcd_backward_small_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_backward_small_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_backward_small_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_equivalentfirstentry. pfgd_pb_gcd_backward_small_witness_common_right = ff_q_pfp_gcd_backward_small_witness_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_backward_small_witness_common_right) + (pfrep_left_gcd_backward_small_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_common_right_equivalentfirstoutside. pfrep_gap_gcd_backward_small_witness_common_right_equivalentfirstoutside+(pfgd_P_gcd_backward_small_witness_common_right)=(pfrep_power_gcd_backward_small_witness_common_right_equivalent)) /\ (((pfrep_left_gcd_backward_small_witness_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_common_right_equivalentsecond. ((pfrep_position_gcd_backward_small_witness_common_right_equivalentsecond+S (pfrep_power_gcd_backward_small_witness_common_right_equivalent)=(R)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_equivalentsecondentry. ff_h_pfp_gcd_backward_small_witness_common_right_equivalentsecondentry + S (pfrep_right_gcd_backward_small_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_backward_small_witness_common_right_equivalentsecond)) * rc)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_equivalentsecondentry. rb = ff_q_pfp_gcd_backward_small_witness_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_common_right_equivalentsecond)) * rc) + (pfrep_right_gcd_backward_small_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_common_right_equivalentsecondoutside. pfrep_gap_gcd_backward_small_witness_common_right_equivalentsecondoutside+(R)=(pfrep_power_gcd_backward_small_witness_common_right_equivalent)) /\ (((pfrep_right_gcd_backward_small_witness_common_right_equivalent)=0))))) -> pfrep_left_gcd_backward_small_witness_common_right_equivalent=pfrep_right_gcd_backward_small_witness_common_right_equivalent)))))))))) /\ ((exists pfgb_pb_gcd_backward_small_witness_bezout pfgb_pc_gcd_backward_small_witness_bezout pfgb_P_gcd_backward_small_witness_bezout pfgb_qb_gcd_backward_small_witness_bezout pfgb_qc_gcd_backward_small_witness_bezout pfgb_Q_gcd_backward_small_witness_bezout. ((((forall fom_index_pfp_gcd_backward_small_witness_bezout_leftleft. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_leftleft_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_leftleft_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_leftleft) = pfgs_U_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_leftleft. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_leftleft_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_leftleft_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_leftleft) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_leftleft)) * pfgs_uc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_leftleft_entry. pfgs_ub_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_leftleft_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_leftleft)) * pfgs_uc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_bezout_leftleft))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_leftleft_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_leftleft_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_bezout_leftright. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_leftright_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_leftright_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_leftright) = S d) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_leftright. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_leftright_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_leftright_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_leftright) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_leftright)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_leftright_entry. bb = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_leftright_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_leftright)) * bc) + (fom_value_pfp_gcd_backward_small_witness_bezout_leftright))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_leftright_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_leftright_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_leftright) = p))) /\ (((((((pfgs_U_gcd_backward_small)=0 \/ (S d)=0) /\ (((pfgb_P_gcd_backward_small_witness_bezout)=0)))) \/ (((~((pfgs_U_gcd_backward_small)=0)) /\ (((~((S d)=0)) /\ (((pfgs_U_gcd_backward_small)+(S d)=S (pfgb_P_gcd_backward_small_witness_bezout)))))))) /\ ((forall pfc_index_gcd_backward_small_witness_bezout_leftcoefficients. (exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientsbound. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientsbound + S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients) = (pfgb_P_gcd_backward_small_witness_bezout)) -> exists pfc_value_gcd_backward_small_witness_bezout_leftcoefficients. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientsentry. ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientsentry + S (pfc_value_gcd_backward_small_witness_bezout_leftcoefficients) = S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_backward_small_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientsentry. pfgb_pb_gcd_backward_small_witness_bezout = ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientsentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_backward_small_witness_bezout) + (pfc_value_gcd_backward_small_witness_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_small_witness_bezout_leftcoefficientscoefficient pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient pfc_natural_sum_gcd_backward_small_witness_bezout_leftcoefficientscoefficient. ((forall pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients))) -> exists pfc_value_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_small_witness_bezout_leftcoefficientscoefficient = ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient) + (pfc_value_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_small_witness_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal) = (pfgs_U_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. pfgs_ub_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_backward_small) + (pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(pfgs_U_gcd_backward_small)=(pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_small_witness_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_small_witness_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients)) -> exists fs_a_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_small_witness_bezout_leftcoefficientscoefficient = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient) + (fs_a_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_small_witness_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_small_witness_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_small_witness_bezout_leftcoefficients) + (p) * pfa_offset_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_gcd_backward_small_witness_bezout_rightleft. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_rightleft_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_rightleft_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_rightleft) = pfgs_V_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_rightleft. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_rightleft_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_rightleft_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_rightleft) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_rightleft)) * pfgs_vc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_rightleft_entry. pfgs_vb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_rightleft_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_rightleft)) * pfgs_vc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_bezout_rightleft))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_rightleft_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_rightleft_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_bezout_rightright. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_rightright_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_rightright_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_rightright) = R) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_rightright. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_rightright_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_rightright_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_rightright) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_rightright)) * rc)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_rightright_entry. rb = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_rightright_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_rightright)) * rc) + (fom_value_pfp_gcd_backward_small_witness_bezout_rightright))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_rightright_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_rightright_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_rightright) = p))) /\ (((((((pfgs_V_gcd_backward_small)=0 \/ (R)=0) /\ (((pfgb_Q_gcd_backward_small_witness_bezout)=0)))) \/ (((~((pfgs_V_gcd_backward_small)=0)) /\ (((~((R)=0)) /\ (((pfgs_V_gcd_backward_small)+(R)=S (pfgb_Q_gcd_backward_small_witness_bezout)))))))) /\ ((forall pfc_index_gcd_backward_small_witness_bezout_rightcoefficients. (exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientsbound. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientsbound + S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients) = (pfgb_Q_gcd_backward_small_witness_bezout)) -> exists pfc_value_gcd_backward_small_witness_bezout_rightcoefficients. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientsentry. ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientsentry + S (pfc_value_gcd_backward_small_witness_bezout_rightcoefficients) = S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_backward_small_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientsentry. pfgb_qb_gcd_backward_small_witness_bezout = ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientsentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_backward_small_witness_bezout) + (pfc_value_gcd_backward_small_witness_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_small_witness_bezout_rightcoefficientscoefficient pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient pfc_natural_sum_gcd_backward_small_witness_bezout_rightcoefficientscoefficient. ((forall pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients))) -> exists pfc_value_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_small_witness_bezout_rightcoefficientscoefficient = ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient) + (pfc_value_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_small_witness_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal) = (pfgs_V_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. pfgs_vb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_backward_small) + (pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(pfgs_V_gcd_backward_small)=(pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm) = (R)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * rc)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. rb = ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * rc) + (pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(R)=(pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_small_witness_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_small_witness_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients)) -> exists fs_a_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_small_witness_bezout_rightcoefficientscoefficient = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient) + (fs_a_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_small_witness_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_small_witness_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_small_witness_bezout_rightcoefficients) + (p) * pfa_offset_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_gcd_backward_small_witness_bezout_sum_left_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_left_bounded) = pfgb_P_gcd_backward_small_witness_bezout) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_left_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_backward_small_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_entry. pfgb_pb_gcd_backward_small_witness_bezout = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_backward_small_witness_bezout) + (fom_value_pfp_gcd_backward_small_witness_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_bezout_sum_right_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_right_bounded) = pfgb_Q_gcd_backward_small_witness_bezout) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_right_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_backward_small_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_entry. pfgb_qb_gcd_backward_small_witness_bezout = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_backward_small_witness_bezout) + (fom_value_pfp_gcd_backward_small_witness_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_bezout_sum_result_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_result_bounded) = pfgs_G_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_result_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_entry. pfgs_gb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_gcd_backward_small_witness_bezout_sum pfga_uc_gcd_backward_small_witness_bezout_sum pfga_vb_gcd_backward_small_witness_bezout_sum pfga_vc_gcd_backward_small_witness_bezout_sum pfga_tb_gcd_backward_small_witness_bezout_sum pfga_tc_gcd_backward_small_witness_bezout_sum pfga_K_gcd_backward_small_witness_bezout_sum. ((((forall pfrep_power_gcd_backward_small_witness_bezout_sum_left pfrep_left_gcd_backward_small_witness_bezout_sum_left pfrep_right_gcd_backward_small_witness_bezout_sum_left. ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_leftfirst. ((pfrep_position_gcd_backward_small_witness_bezout_sum_leftfirst+S (pfrep_power_gcd_backward_small_witness_bezout_sum_left)=(pfgb_P_gcd_backward_small_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_leftfirstentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_leftfirstentry + S (pfrep_left_gcd_backward_small_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_backward_small_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_leftfirstentry. pfgb_pb_gcd_backward_small_witness_bezout = ff_q_pfp_gcd_backward_small_witness_bezout_sum_leftfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_backward_small_witness_bezout) + (pfrep_left_gcd_backward_small_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_leftfirstoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_leftfirstoutside+(pfgb_P_gcd_backward_small_witness_bezout)=(pfrep_power_gcd_backward_small_witness_bezout_sum_left)) /\ (((pfrep_left_gcd_backward_small_witness_bezout_sum_left)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_leftsecond. ((pfrep_position_gcd_backward_small_witness_bezout_sum_leftsecond+S (pfrep_power_gcd_backward_small_witness_bezout_sum_left)=(pfga_K_gcd_backward_small_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_leftsecondentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_leftsecondentry + S (pfrep_right_gcd_backward_small_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_leftsecondentry. pfga_ub_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_leftsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_backward_small_witness_bezout_sum) + (pfrep_right_gcd_backward_small_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_leftsecondoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_leftsecondoutside+(pfga_K_gcd_backward_small_witness_bezout_sum)=(pfrep_power_gcd_backward_small_witness_bezout_sum_left)) /\ (((pfrep_right_gcd_backward_small_witness_bezout_sum_left)=0))))) -> pfrep_left_gcd_backward_small_witness_bezout_sum_left=pfrep_right_gcd_backward_small_witness_bezout_sum_left) /\ ((forall pfrep_power_gcd_backward_small_witness_bezout_sum_right pfrep_left_gcd_backward_small_witness_bezout_sum_right pfrep_right_gcd_backward_small_witness_bezout_sum_right. ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_rightfirst. ((pfrep_position_gcd_backward_small_witness_bezout_sum_rightfirst+S (pfrep_power_gcd_backward_small_witness_bezout_sum_right)=(pfgb_Q_gcd_backward_small_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_rightfirstentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_rightfirstentry + S (pfrep_left_gcd_backward_small_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_backward_small_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_rightfirstentry. pfgb_qb_gcd_backward_small_witness_bezout = ff_q_pfp_gcd_backward_small_witness_bezout_sum_rightfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_backward_small_witness_bezout) + (pfrep_left_gcd_backward_small_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_rightfirstoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_rightfirstoutside+(pfgb_Q_gcd_backward_small_witness_bezout)=(pfrep_power_gcd_backward_small_witness_bezout_sum_right)) /\ (((pfrep_left_gcd_backward_small_witness_bezout_sum_right)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_rightsecond. ((pfrep_position_gcd_backward_small_witness_bezout_sum_rightsecond+S (pfrep_power_gcd_backward_small_witness_bezout_sum_right)=(pfga_K_gcd_backward_small_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_rightsecondentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_rightsecondentry + S (pfrep_right_gcd_backward_small_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_rightsecondentry. pfga_vb_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_rightsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_backward_small_witness_bezout_sum) + (pfrep_right_gcd_backward_small_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_rightsecondoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_rightsecondoutside+(pfga_K_gcd_backward_small_witness_bezout_sum)=(pfrep_power_gcd_backward_small_witness_bezout_sum_right)) /\ (((pfrep_right_gcd_backward_small_witness_bezout_sum_right)=0))))) -> pfrep_left_gcd_backward_small_witness_bezout_sum_right=pfrep_right_gcd_backward_small_witness_bezout_sum_right)))) /\ (((forall pfp_index_gcd_backward_small_witness_bezout_sum_add. (exists pfa_gap_gcd_backward_small_witness_bezout_sum_addindex. pfa_gap_gcd_backward_small_witness_bezout_sum_addindex + S (pfp_index_gcd_backward_small_witness_bezout_sum_add) = (pfga_K_gcd_backward_small_witness_bezout_sum)) -> exists pfp_left_gcd_backward_small_witness_bezout_sum_add pfp_right_gcd_backward_small_witness_bezout_sum_add pfp_value_gcd_backward_small_witness_bezout_sum_add. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_addleft. ff_h_pfp_gcd_backward_small_witness_bezout_sum_addleft + S (pfp_left_gcd_backward_small_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_uc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_addleft. pfga_ub_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_addleft * S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_uc_gcd_backward_small_witness_bezout_sum) + (pfp_left_gcd_backward_small_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_addright. ff_h_pfp_gcd_backward_small_witness_bezout_sum_addright + S (pfp_right_gcd_backward_small_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_vc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_addright. pfga_vb_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_addright * S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_vc_gcd_backward_small_witness_bezout_sum) + (pfp_right_gcd_backward_small_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_addtarget. ff_h_pfp_gcd_backward_small_witness_bezout_sum_addtarget + S (pfp_value_gcd_backward_small_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_tc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_addtarget. pfga_tb_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_addtarget * S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_tc_gcd_backward_small_witness_bezout_sum) + (pfp_value_gcd_backward_small_witness_bezout_sum_add))) /\ ((((exists pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationleft. pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationleft + S (pfp_left_gcd_backward_small_witness_bezout_sum_add) = (p)) /\ (((exists pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationright. pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationright + S (pfp_right_gcd_backward_small_witness_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationresultbound. pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationresultbound + S (pfp_value_gcd_backward_small_witness_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_bezout_sum_addoperationresultcongruence pfa_offset_right_gcd_backward_small_witness_bezout_sum_addoperationresultcongruence. ((pfp_left_gcd_backward_small_witness_bezout_sum_add) + (pfp_right_gcd_backward_small_witness_bezout_sum_add)) + (p) * pfa_offset_left_gcd_backward_small_witness_bezout_sum_addoperationresultcongruence = (pfp_value_gcd_backward_small_witness_bezout_sum_add) + (p) * pfa_offset_right_gcd_backward_small_witness_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_gcd_backward_small_witness_bezout_sum_result pfrep_left_gcd_backward_small_witness_bezout_sum_result pfrep_right_gcd_backward_small_witness_bezout_sum_result. ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_resultfirst. ((pfrep_position_gcd_backward_small_witness_bezout_sum_resultfirst+S (pfrep_power_gcd_backward_small_witness_bezout_sum_result)=(pfga_K_gcd_backward_small_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_resultfirstentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_resultfirstentry + S (pfrep_left_gcd_backward_small_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_resultfirstentry. pfga_tb_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_resultfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_backward_small_witness_bezout_sum) + (pfrep_left_gcd_backward_small_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_resultfirstoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_resultfirstoutside+(pfga_K_gcd_backward_small_witness_bezout_sum)=(pfrep_power_gcd_backward_small_witness_bezout_sum_result)) /\ (((pfrep_left_gcd_backward_small_witness_bezout_sum_result)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_resultsecond. ((pfrep_position_gcd_backward_small_witness_bezout_sum_resultsecond+S (pfrep_power_gcd_backward_small_witness_bezout_sum_result)=(pfgs_G_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_resultsecondentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_resultsecondentry + S (pfrep_right_gcd_backward_small_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_resultsecondentry. pfgs_gb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_bezout_sum_resultsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_backward_small) + (pfrep_right_gcd_backward_small_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_resultsecondoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_resultsecondoutside+(pfgs_G_gcd_backward_small)=(pfrep_power_gcd_backward_small_witness_bezout_sum_result)) /\ (((pfrep_right_gcd_backward_small_witness_bezout_sum_result)=0))))) -> pfrep_left_gcd_backward_small_witness_bezout_sum_result=pfrep_right_gcd_backward_small_witness_bezout_sum_result))))))))))))))))))))))) -> (exists pfgs_gb_gcd_backward_result pfgs_gc_gcd_backward_result pfgs_G_gcd_backward_result pfgs_ub_gcd_backward_result pfgs_uc_gcd_backward_result pfgs_U_gcd_backward_result pfgs_vb_gcd_backward_result pfgs_vc_gcd_backward_result pfgs_V_gcd_backward_result. (((pfgs_G_gcd_backward_result)=0 \/ (((~((pfgs_G_gcd_backward_result) = 0)) /\ (((forall fom_index_pfp_gcd_backward_result_witness_normal_moniccoefficients. (exists fom_gap_pfp_gcd_backward_result_witness_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_backward_result_witness_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_backward_result_witness_normal_moniccoefficients) = pfgs_G_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_backward_result_witness_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_backward_result_witness_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_backward_result_witness_normal_moniccoefficients)) * pfgs_gc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_normal_moniccoefficients_entry. pfgs_gb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_normal_moniccoefficients)) * pfgs_gc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_backward_result_witness_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_backward_result_witness_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_normal_monicleading. ff_h_pfp_gcd_backward_result_witness_normal_monicleading + S (1) = S ((S (0)) * pfgs_gc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_normal_monicleading. pfgs_gb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_normal_monicleading * S ((S (0)) * pfgs_gc_gcd_backward_result) + (1))))))))) /\ (((((((forall fom_index_pfp_gcd_backward_result_witness_common_left_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_common_left_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_left_bounded) = L) -> exists fom_value_pfp_gcd_backward_result_witness_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_left_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_left_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_common_left_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_bounded_entry. ab = fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_bounded)) * ac) + (fom_value_pfp_gcd_backward_result_witness_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_left_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_backward_result_witness_common_left pfgd_qc_gcd_backward_result_witness_common_left pfgd_Q_gcd_backward_result_witness_common_left pfgd_pb_gcd_backward_result_witness_common_left pfgd_pc_gcd_backward_result_witness_common_left pfgd_P_gcd_backward_result_witness_common_left. ((((forall fom_index_pfp_gcd_backward_result_witness_common_left_productleft. (exists fom_gap_pfp_gcd_backward_result_witness_common_left_productleft_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_productleft_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_left_productleft) = pfgd_Q_gcd_backward_result_witness_common_left) -> exists fom_value_pfp_gcd_backward_result_witness_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_left_productleft_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_left_productleft_entry + S (fom_value_pfp_gcd_backward_result_witness_common_left_productleft) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_productleft)) * pfgd_qc_gcd_backward_result_witness_common_left)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_productleft_entry. pfgd_qb_gcd_backward_result_witness_common_left = fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_productleft)) * pfgd_qc_gcd_backward_result_witness_common_left) + (fom_value_pfp_gcd_backward_result_witness_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_left_productleft_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_productleft_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_common_left_productright. (exists fom_gap_pfp_gcd_backward_result_witness_common_left_productright_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_productright_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_left_productright) = pfgs_G_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_common_left_productright. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_left_productright_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_left_productright_entry + S (fom_value_pfp_gcd_backward_result_witness_common_left_productright) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_productright)) * pfgs_gc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_productright_entry. pfgs_gb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_productright_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_productright)) * pfgs_gc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_common_left_productright))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_left_productright_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_productright_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_backward_result_witness_common_left)=0 \/ (pfgs_G_gcd_backward_result)=0) /\ (((pfgd_P_gcd_backward_result_witness_common_left)=0)))) \/ (((~((pfgd_Q_gcd_backward_result_witness_common_left)=0)) /\ (((~((pfgs_G_gcd_backward_result)=0)) /\ (((pfgd_Q_gcd_backward_result_witness_common_left)+(pfgs_G_gcd_backward_result)=S (pfgd_P_gcd_backward_result_witness_common_left)))))))) /\ ((forall pfc_index_gcd_backward_result_witness_common_left_productcoefficients. (exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientsbound. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientsbound + S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients) = (pfgd_P_gcd_backward_result_witness_common_left)) -> exists pfc_value_gcd_backward_result_witness_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientsentry. ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientsentry + S (pfc_value_gcd_backward_result_witness_common_left_productcoefficients) = S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients)) * pfgd_pc_gcd_backward_result_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientsentry. pfgd_pb_gcd_backward_result_witness_common_left = ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients)) * pfgd_pc_gcd_backward_result_witness_common_left) + (pfc_value_gcd_backward_result_witness_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_result_witness_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_backward_result_witness_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients))) -> exists pfc_value_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_result_witness_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient) + (pfc_value_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_result_witness_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_backward_result_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_result_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_backward_result_witness_common_left = ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_result_witness_common_left) + (pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_backward_result_witness_common_left)=(pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_result) + (pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_backward_result)=(pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_result_witness_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_result_witness_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_result_witness_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_result_witness_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_result_witness_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_result_witness_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_backward_result_witness_common_left_equivalent pfrep_left_gcd_backward_result_witness_common_left_equivalent pfrep_right_gcd_backward_result_witness_common_left_equivalent. ((exists pfrep_position_gcd_backward_result_witness_common_left_equivalentfirst. ((pfrep_position_gcd_backward_result_witness_common_left_equivalentfirst+S (pfrep_power_gcd_backward_result_witness_common_left_equivalent)=(pfgd_P_gcd_backward_result_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_equivalentfirstentry. ff_h_pfp_gcd_backward_result_witness_common_left_equivalentfirstentry + S (pfrep_left_gcd_backward_result_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_backward_result_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_backward_result_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_equivalentfirstentry. pfgd_pb_gcd_backward_result_witness_common_left = ff_q_pfp_gcd_backward_result_witness_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_backward_result_witness_common_left) + (pfrep_left_gcd_backward_result_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_common_left_equivalentfirstoutside. pfrep_gap_gcd_backward_result_witness_common_left_equivalentfirstoutside+(pfgd_P_gcd_backward_result_witness_common_left)=(pfrep_power_gcd_backward_result_witness_common_left_equivalent)) /\ (((pfrep_left_gcd_backward_result_witness_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_common_left_equivalentsecond. ((pfrep_position_gcd_backward_result_witness_common_left_equivalentsecond+S (pfrep_power_gcd_backward_result_witness_common_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_equivalentsecondentry. ff_h_pfp_gcd_backward_result_witness_common_left_equivalentsecondentry + S (pfrep_right_gcd_backward_result_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_backward_result_witness_common_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_equivalentsecondentry. ab = ff_q_pfp_gcd_backward_result_witness_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_common_left_equivalentsecond)) * ac) + (pfrep_right_gcd_backward_result_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_common_left_equivalentsecondoutside. pfrep_gap_gcd_backward_result_witness_common_left_equivalentsecondoutside+(L)=(pfrep_power_gcd_backward_result_witness_common_left_equivalent)) /\ (((pfrep_right_gcd_backward_result_witness_common_left_equivalent)=0))))) -> pfrep_left_gcd_backward_result_witness_common_left_equivalent=pfrep_right_gcd_backward_result_witness_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_backward_result_witness_common_right_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_common_right_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_right_bounded) = S d) -> exists fom_value_pfp_gcd_backward_result_witness_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_right_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_right_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_common_right_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_bounded_entry. bb = fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_bounded)) * bc) + (fom_value_pfp_gcd_backward_result_witness_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_right_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_backward_result_witness_common_right pfgd_qc_gcd_backward_result_witness_common_right pfgd_Q_gcd_backward_result_witness_common_right pfgd_pb_gcd_backward_result_witness_common_right pfgd_pc_gcd_backward_result_witness_common_right pfgd_P_gcd_backward_result_witness_common_right. ((((forall fom_index_pfp_gcd_backward_result_witness_common_right_productleft. (exists fom_gap_pfp_gcd_backward_result_witness_common_right_productleft_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_productleft_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_right_productleft) = pfgd_Q_gcd_backward_result_witness_common_right) -> exists fom_value_pfp_gcd_backward_result_witness_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_right_productleft_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_right_productleft_entry + S (fom_value_pfp_gcd_backward_result_witness_common_right_productleft) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_productleft)) * pfgd_qc_gcd_backward_result_witness_common_right)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_productleft_entry. pfgd_qb_gcd_backward_result_witness_common_right = fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_productleft)) * pfgd_qc_gcd_backward_result_witness_common_right) + (fom_value_pfp_gcd_backward_result_witness_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_right_productleft_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_productleft_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_common_right_productright. (exists fom_gap_pfp_gcd_backward_result_witness_common_right_productright_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_productright_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_right_productright) = pfgs_G_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_common_right_productright. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_right_productright_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_right_productright_entry + S (fom_value_pfp_gcd_backward_result_witness_common_right_productright) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_productright)) * pfgs_gc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_productright_entry. pfgs_gb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_productright_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_productright)) * pfgs_gc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_common_right_productright))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_right_productright_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_productright_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_backward_result_witness_common_right)=0 \/ (pfgs_G_gcd_backward_result)=0) /\ (((pfgd_P_gcd_backward_result_witness_common_right)=0)))) \/ (((~((pfgd_Q_gcd_backward_result_witness_common_right)=0)) /\ (((~((pfgs_G_gcd_backward_result)=0)) /\ (((pfgd_Q_gcd_backward_result_witness_common_right)+(pfgs_G_gcd_backward_result)=S (pfgd_P_gcd_backward_result_witness_common_right)))))))) /\ ((forall pfc_index_gcd_backward_result_witness_common_right_productcoefficients. (exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientsbound. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientsbound + S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients) = (pfgd_P_gcd_backward_result_witness_common_right)) -> exists pfc_value_gcd_backward_result_witness_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientsentry. ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientsentry + S (pfc_value_gcd_backward_result_witness_common_right_productcoefficients) = S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients)) * pfgd_pc_gcd_backward_result_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientsentry. pfgd_pb_gcd_backward_result_witness_common_right = ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients)) * pfgd_pc_gcd_backward_result_witness_common_right) + (pfc_value_gcd_backward_result_witness_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_result_witness_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_backward_result_witness_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients))) -> exists pfc_value_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_result_witness_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient) + (pfc_value_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_result_witness_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_backward_result_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_result_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_backward_result_witness_common_right = ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_result_witness_common_right) + (pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_backward_result_witness_common_right)=(pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_result) + (pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_backward_result)=(pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_result_witness_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_result_witness_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_result_witness_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_result_witness_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_result_witness_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_result_witness_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_backward_result_witness_common_right_equivalent pfrep_left_gcd_backward_result_witness_common_right_equivalent pfrep_right_gcd_backward_result_witness_common_right_equivalent. ((exists pfrep_position_gcd_backward_result_witness_common_right_equivalentfirst. ((pfrep_position_gcd_backward_result_witness_common_right_equivalentfirst+S (pfrep_power_gcd_backward_result_witness_common_right_equivalent)=(pfgd_P_gcd_backward_result_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_equivalentfirstentry. ff_h_pfp_gcd_backward_result_witness_common_right_equivalentfirstentry + S (pfrep_left_gcd_backward_result_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_backward_result_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_backward_result_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_equivalentfirstentry. pfgd_pb_gcd_backward_result_witness_common_right = ff_q_pfp_gcd_backward_result_witness_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_backward_result_witness_common_right) + (pfrep_left_gcd_backward_result_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_common_right_equivalentfirstoutside. pfrep_gap_gcd_backward_result_witness_common_right_equivalentfirstoutside+(pfgd_P_gcd_backward_result_witness_common_right)=(pfrep_power_gcd_backward_result_witness_common_right_equivalent)) /\ (((pfrep_left_gcd_backward_result_witness_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_common_right_equivalentsecond. ((pfrep_position_gcd_backward_result_witness_common_right_equivalentsecond+S (pfrep_power_gcd_backward_result_witness_common_right_equivalent)=(S d)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_equivalentsecondentry. ff_h_pfp_gcd_backward_result_witness_common_right_equivalentsecondentry + S (pfrep_right_gcd_backward_result_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_backward_result_witness_common_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_equivalentsecondentry. bb = ff_q_pfp_gcd_backward_result_witness_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_common_right_equivalentsecond)) * bc) + (pfrep_right_gcd_backward_result_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_common_right_equivalentsecondoutside. pfrep_gap_gcd_backward_result_witness_common_right_equivalentsecondoutside+(S d)=(pfrep_power_gcd_backward_result_witness_common_right_equivalent)) /\ (((pfrep_right_gcd_backward_result_witness_common_right_equivalent)=0))))) -> pfrep_left_gcd_backward_result_witness_common_right_equivalent=pfrep_right_gcd_backward_result_witness_common_right_equivalent)))))))))) /\ ((exists pfgb_pb_gcd_backward_result_witness_bezout pfgb_pc_gcd_backward_result_witness_bezout pfgb_P_gcd_backward_result_witness_bezout pfgb_qb_gcd_backward_result_witness_bezout pfgb_qc_gcd_backward_result_witness_bezout pfgb_Q_gcd_backward_result_witness_bezout. ((((forall fom_index_pfp_gcd_backward_result_witness_bezout_leftleft. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_leftleft_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_leftleft_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_leftleft) = pfgs_U_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_leftleft. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_leftleft_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_leftleft_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_leftleft) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_leftleft)) * pfgs_uc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_leftleft_entry. pfgs_ub_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_leftleft_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_leftleft)) * pfgs_uc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_bezout_leftleft))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_leftleft_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_leftleft_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_bezout_leftright. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_leftright_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_leftright_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_leftright) = L) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_leftright. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_leftright_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_leftright_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_leftright) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_leftright)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_leftright_entry. ab = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_leftright_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_leftright)) * ac) + (fom_value_pfp_gcd_backward_result_witness_bezout_leftright))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_leftright_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_leftright_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_leftright) = p))) /\ (((((((pfgs_U_gcd_backward_result)=0 \/ (L)=0) /\ (((pfgb_P_gcd_backward_result_witness_bezout)=0)))) \/ (((~((pfgs_U_gcd_backward_result)=0)) /\ (((~((L)=0)) /\ (((pfgs_U_gcd_backward_result)+(L)=S (pfgb_P_gcd_backward_result_witness_bezout)))))))) /\ ((forall pfc_index_gcd_backward_result_witness_bezout_leftcoefficients. (exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientsbound. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientsbound + S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients) = (pfgb_P_gcd_backward_result_witness_bezout)) -> exists pfc_value_gcd_backward_result_witness_bezout_leftcoefficients. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientsentry. ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientsentry + S (pfc_value_gcd_backward_result_witness_bezout_leftcoefficients) = S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_backward_result_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientsentry. pfgb_pb_gcd_backward_result_witness_bezout = ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientsentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_backward_result_witness_bezout) + (pfc_value_gcd_backward_result_witness_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_result_witness_bezout_leftcoefficientscoefficient pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient pfc_natural_sum_gcd_backward_result_witness_bezout_leftcoefficientscoefficient. ((forall pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients))) -> exists pfc_value_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_result_witness_bezout_leftcoefficientscoefficient = ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient) + (pfc_value_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_result_witness_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal) = (pfgs_U_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. pfgs_ub_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_backward_result) + (pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(pfgs_U_gcd_backward_result)=(pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_result_witness_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_result_witness_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients)) -> exists fs_a_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_result_witness_bezout_leftcoefficientscoefficient = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient) + (fs_a_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_result_witness_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_result_witness_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_result_witness_bezout_leftcoefficients) + (p) * pfa_offset_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_gcd_backward_result_witness_bezout_rightleft. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_rightleft_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_rightleft_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_rightleft) = pfgs_V_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_rightleft. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_rightleft_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_rightleft_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_rightleft) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_rightleft)) * pfgs_vc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_rightleft_entry. pfgs_vb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_rightleft_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_rightleft)) * pfgs_vc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_bezout_rightleft))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_rightleft_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_rightleft_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_bezout_rightright. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_rightright_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_rightright_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_rightright) = S d) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_rightright. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_rightright_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_rightright_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_rightright) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_rightright_entry. bb = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_rightright_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_rightright)) * bc) + (fom_value_pfp_gcd_backward_result_witness_bezout_rightright))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_rightright_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_rightright_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_rightright) = p))) /\ (((((((pfgs_V_gcd_backward_result)=0 \/ (S d)=0) /\ (((pfgb_Q_gcd_backward_result_witness_bezout)=0)))) \/ (((~((pfgs_V_gcd_backward_result)=0)) /\ (((~((S d)=0)) /\ (((pfgs_V_gcd_backward_result)+(S d)=S (pfgb_Q_gcd_backward_result_witness_bezout)))))))) /\ ((forall pfc_index_gcd_backward_result_witness_bezout_rightcoefficients. (exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientsbound. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientsbound + S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients) = (pfgb_Q_gcd_backward_result_witness_bezout)) -> exists pfc_value_gcd_backward_result_witness_bezout_rightcoefficients. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientsentry. ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientsentry + S (pfc_value_gcd_backward_result_witness_bezout_rightcoefficients) = S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_backward_result_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientsentry. pfgb_qb_gcd_backward_result_witness_bezout = ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientsentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_backward_result_witness_bezout) + (pfc_value_gcd_backward_result_witness_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_result_witness_bezout_rightcoefficientscoefficient pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient pfc_natural_sum_gcd_backward_result_witness_bezout_rightcoefficientscoefficient. ((forall pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients))) -> exists pfc_value_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_result_witness_bezout_rightcoefficientscoefficient = ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient) + (pfc_value_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_result_witness_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal) = (pfgs_V_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. pfgs_vb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_backward_result) + (pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(pfgs_V_gcd_backward_result)=(pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_result_witness_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_result_witness_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients)) -> exists fs_a_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_result_witness_bezout_rightcoefficientscoefficient = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient) + (fs_a_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_result_witness_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_result_witness_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_result_witness_bezout_rightcoefficients) + (p) * pfa_offset_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_gcd_backward_result_witness_bezout_sum_left_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_left_bounded) = pfgb_P_gcd_backward_result_witness_bezout) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_left_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_backward_result_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_entry. pfgb_pb_gcd_backward_result_witness_bezout = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_backward_result_witness_bezout) + (fom_value_pfp_gcd_backward_result_witness_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_bezout_sum_right_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_right_bounded) = pfgb_Q_gcd_backward_result_witness_bezout) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_right_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_backward_result_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_entry. pfgb_qb_gcd_backward_result_witness_bezout = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_backward_result_witness_bezout) + (fom_value_pfp_gcd_backward_result_witness_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_bezout_sum_result_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_result_bounded) = pfgs_G_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_result_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_entry. pfgs_gb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_gcd_backward_result_witness_bezout_sum pfga_uc_gcd_backward_result_witness_bezout_sum pfga_vb_gcd_backward_result_witness_bezout_sum pfga_vc_gcd_backward_result_witness_bezout_sum pfga_tb_gcd_backward_result_witness_bezout_sum pfga_tc_gcd_backward_result_witness_bezout_sum pfga_K_gcd_backward_result_witness_bezout_sum. ((((forall pfrep_power_gcd_backward_result_witness_bezout_sum_left pfrep_left_gcd_backward_result_witness_bezout_sum_left pfrep_right_gcd_backward_result_witness_bezout_sum_left. ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_leftfirst. ((pfrep_position_gcd_backward_result_witness_bezout_sum_leftfirst+S (pfrep_power_gcd_backward_result_witness_bezout_sum_left)=(pfgb_P_gcd_backward_result_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_leftfirstentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_leftfirstentry + S (pfrep_left_gcd_backward_result_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_backward_result_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_leftfirstentry. pfgb_pb_gcd_backward_result_witness_bezout = ff_q_pfp_gcd_backward_result_witness_bezout_sum_leftfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_backward_result_witness_bezout) + (pfrep_left_gcd_backward_result_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_leftfirstoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_leftfirstoutside+(pfgb_P_gcd_backward_result_witness_bezout)=(pfrep_power_gcd_backward_result_witness_bezout_sum_left)) /\ (((pfrep_left_gcd_backward_result_witness_bezout_sum_left)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_leftsecond. ((pfrep_position_gcd_backward_result_witness_bezout_sum_leftsecond+S (pfrep_power_gcd_backward_result_witness_bezout_sum_left)=(pfga_K_gcd_backward_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_leftsecondentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_leftsecondentry + S (pfrep_right_gcd_backward_result_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_leftsecondentry. pfga_ub_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_leftsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_backward_result_witness_bezout_sum) + (pfrep_right_gcd_backward_result_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_leftsecondoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_leftsecondoutside+(pfga_K_gcd_backward_result_witness_bezout_sum)=(pfrep_power_gcd_backward_result_witness_bezout_sum_left)) /\ (((pfrep_right_gcd_backward_result_witness_bezout_sum_left)=0))))) -> pfrep_left_gcd_backward_result_witness_bezout_sum_left=pfrep_right_gcd_backward_result_witness_bezout_sum_left) /\ ((forall pfrep_power_gcd_backward_result_witness_bezout_sum_right pfrep_left_gcd_backward_result_witness_bezout_sum_right pfrep_right_gcd_backward_result_witness_bezout_sum_right. ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_rightfirst. ((pfrep_position_gcd_backward_result_witness_bezout_sum_rightfirst+S (pfrep_power_gcd_backward_result_witness_bezout_sum_right)=(pfgb_Q_gcd_backward_result_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_rightfirstentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_rightfirstentry + S (pfrep_left_gcd_backward_result_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_backward_result_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_rightfirstentry. pfgb_qb_gcd_backward_result_witness_bezout = ff_q_pfp_gcd_backward_result_witness_bezout_sum_rightfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_backward_result_witness_bezout) + (pfrep_left_gcd_backward_result_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_rightfirstoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_rightfirstoutside+(pfgb_Q_gcd_backward_result_witness_bezout)=(pfrep_power_gcd_backward_result_witness_bezout_sum_right)) /\ (((pfrep_left_gcd_backward_result_witness_bezout_sum_right)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_rightsecond. ((pfrep_position_gcd_backward_result_witness_bezout_sum_rightsecond+S (pfrep_power_gcd_backward_result_witness_bezout_sum_right)=(pfga_K_gcd_backward_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_rightsecondentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_rightsecondentry + S (pfrep_right_gcd_backward_result_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_rightsecondentry. pfga_vb_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_rightsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_backward_result_witness_bezout_sum) + (pfrep_right_gcd_backward_result_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_rightsecondoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_rightsecondoutside+(pfga_K_gcd_backward_result_witness_bezout_sum)=(pfrep_power_gcd_backward_result_witness_bezout_sum_right)) /\ (((pfrep_right_gcd_backward_result_witness_bezout_sum_right)=0))))) -> pfrep_left_gcd_backward_result_witness_bezout_sum_right=pfrep_right_gcd_backward_result_witness_bezout_sum_right)))) /\ (((forall pfp_index_gcd_backward_result_witness_bezout_sum_add. (exists pfa_gap_gcd_backward_result_witness_bezout_sum_addindex. pfa_gap_gcd_backward_result_witness_bezout_sum_addindex + S (pfp_index_gcd_backward_result_witness_bezout_sum_add) = (pfga_K_gcd_backward_result_witness_bezout_sum)) -> exists pfp_left_gcd_backward_result_witness_bezout_sum_add pfp_right_gcd_backward_result_witness_bezout_sum_add pfp_value_gcd_backward_result_witness_bezout_sum_add. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_addleft. ff_h_pfp_gcd_backward_result_witness_bezout_sum_addleft + S (pfp_left_gcd_backward_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_uc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_addleft. pfga_ub_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_addleft * S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_uc_gcd_backward_result_witness_bezout_sum) + (pfp_left_gcd_backward_result_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_addright. ff_h_pfp_gcd_backward_result_witness_bezout_sum_addright + S (pfp_right_gcd_backward_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_vc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_addright. pfga_vb_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_addright * S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_vc_gcd_backward_result_witness_bezout_sum) + (pfp_right_gcd_backward_result_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_addtarget. ff_h_pfp_gcd_backward_result_witness_bezout_sum_addtarget + S (pfp_value_gcd_backward_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_tc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_addtarget. pfga_tb_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_addtarget * S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_tc_gcd_backward_result_witness_bezout_sum) + (pfp_value_gcd_backward_result_witness_bezout_sum_add))) /\ ((((exists pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationleft. pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationleft + S (pfp_left_gcd_backward_result_witness_bezout_sum_add) = (p)) /\ (((exists pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationright. pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationright + S (pfp_right_gcd_backward_result_witness_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationresultbound. pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationresultbound + S (pfp_value_gcd_backward_result_witness_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_bezout_sum_addoperationresultcongruence pfa_offset_right_gcd_backward_result_witness_bezout_sum_addoperationresultcongruence. ((pfp_left_gcd_backward_result_witness_bezout_sum_add) + (pfp_right_gcd_backward_result_witness_bezout_sum_add)) + (p) * pfa_offset_left_gcd_backward_result_witness_bezout_sum_addoperationresultcongruence = (pfp_value_gcd_backward_result_witness_bezout_sum_add) + (p) * pfa_offset_right_gcd_backward_result_witness_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_gcd_backward_result_witness_bezout_sum_result pfrep_left_gcd_backward_result_witness_bezout_sum_result pfrep_right_gcd_backward_result_witness_bezout_sum_result. ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_resultfirst. ((pfrep_position_gcd_backward_result_witness_bezout_sum_resultfirst+S (pfrep_power_gcd_backward_result_witness_bezout_sum_result)=(pfga_K_gcd_backward_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_resultfirstentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_resultfirstentry + S (pfrep_left_gcd_backward_result_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_resultfirstentry. pfga_tb_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_resultfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_backward_result_witness_bezout_sum) + (pfrep_left_gcd_backward_result_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_resultfirstoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_resultfirstoutside+(pfga_K_gcd_backward_result_witness_bezout_sum)=(pfrep_power_gcd_backward_result_witness_bezout_sum_result)) /\ (((pfrep_left_gcd_backward_result_witness_bezout_sum_result)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_resultsecond. ((pfrep_position_gcd_backward_result_witness_bezout_sum_resultsecond+S (pfrep_power_gcd_backward_result_witness_bezout_sum_result)=(pfgs_G_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_resultsecondentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_resultsecondentry + S (pfrep_right_gcd_backward_result_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_resultsecondentry. pfgs_gb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_bezout_sum_resultsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_backward_result) + (pfrep_right_gcd_backward_result_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_resultsecondoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_resultsecondoutside+(pfgs_G_gcd_backward_result)=(pfrep_power_gcd_backward_result_witness_bezout_sum_result)) /\ (((pfrep_right_gcd_backward_result_witness_bezout_sum_result)=0))))) -> pfrep_left_gcd_backward_result_witness_bezout_sum_result=pfrep_right_gcd_backward_result_witness_bezout_sum_result)))))))))))))))))))))))