prime_field_polynomial_common_right_divisor_euclidean_transport

Exact expanded first-order arithmetic statement

forall p db dc J ab ac L bb bc M qb qc H pb pc I rb rc N. (~((p) = 1) /\ forall pfa_factor_left_euclidean_common_prime pfa_factor_right_euclidean_common_prime. (p) = pfa_factor_left_euclidean_common_prime * pfa_factor_right_euclidean_common_prime -> pfa_factor_left_euclidean_common_prime = 1 \/ pfa_factor_right_euclidean_common_prime = 1) -> (((forall fom_index_pfp_euclidean_common_productleft. (exists fom_gap_pfp_euclidean_common_productleft_index_bound. fom_gap_pfp_euclidean_common_productleft_index_bound + S (fom_index_pfp_euclidean_common_productleft) = H) -> exists fom_value_pfp_euclidean_common_productleft. ((((exists fom_beta_height_pfp_euclidean_common_productleft_entry. fom_beta_height_pfp_euclidean_common_productleft_entry + S (fom_value_pfp_euclidean_common_productleft) = S ((S (fom_index_pfp_euclidean_common_productleft)) * qc)) /\ exists fom_beta_quotient_pfp_euclidean_common_productleft_entry. qb = fom_beta_quotient_pfp_euclidean_common_productleft_entry * S ((S (fom_index_pfp_euclidean_common_productleft)) * qc) + (fom_value_pfp_euclidean_common_productleft))) /\ (exists fom_gap_pfp_euclidean_common_productleft_value_bound. fom_gap_pfp_euclidean_common_productleft_value_bound + S (fom_value_pfp_euclidean_common_productleft) = p))) /\ (((forall fom_index_pfp_euclidean_common_productright. (exists fom_gap_pfp_euclidean_common_productright_index_bound. fom_gap_pfp_euclidean_common_productright_index_bound + S (fom_index_pfp_euclidean_common_productright) = M) -> exists fom_value_pfp_euclidean_common_productright. ((((exists fom_beta_height_pfp_euclidean_common_productright_entry. fom_beta_height_pfp_euclidean_common_productright_entry + S (fom_value_pfp_euclidean_common_productright) = S ((S (fom_index_pfp_euclidean_common_productright)) * bc)) /\ exists fom_beta_quotient_pfp_euclidean_common_productright_entry. bb = fom_beta_quotient_pfp_euclidean_common_productright_entry * S ((S (fom_index_pfp_euclidean_common_productright)) * bc) + (fom_value_pfp_euclidean_common_productright))) /\ (exists fom_gap_pfp_euclidean_common_productright_value_bound. fom_gap_pfp_euclidean_common_productright_value_bound + S (fom_value_pfp_euclidean_common_productright) = p))) /\ (((((((H)=0 \/ (M)=0) /\ (((I)=0)))) \/ (((~((H)=0)) /\ (((~((M)=0)) /\ (((H)+(M)=S (I)))))))) /\ ((forall pfc_index_euclidean_common_productcoefficients. (exists pfa_gap_euclidean_common_productcoefficientsbound. pfa_gap_euclidean_common_productcoefficientsbound + S (pfc_index_euclidean_common_productcoefficients) = (I)) -> exists pfc_value_euclidean_common_productcoefficients. ((((exists ff_h_pfp_euclidean_common_productcoefficientsentry. ff_h_pfp_euclidean_common_productcoefficientsentry + S (pfc_value_euclidean_common_productcoefficients) = S ((S (pfc_index_euclidean_common_productcoefficients)) * pc)) /\ exists ff_q_pfp_euclidean_common_productcoefficientsentry. pb = ff_q_pfp_euclidean_common_productcoefficientsentry * S ((S (pfc_index_euclidean_common_productcoefficients)) * pc) + (pfc_value_euclidean_common_productcoefficients))) /\ ((exists pfc_terms_code_euclidean_common_productcoefficientscoefficient pfc_terms_scale_euclidean_common_productcoefficientscoefficient pfc_natural_sum_euclidean_common_productcoefficientscoefficient. ((forall pfc_index_euclidean_common_productcoefficientscoefficientdiagonal. (exists pfa_gap_euclidean_common_productcoefficientscoefficientdiagonalbound. pfa_gap_euclidean_common_productcoefficientscoefficientdiagonalbound + S (pfc_index_euclidean_common_productcoefficientscoefficientdiagonal) = (S (pfc_index_euclidean_common_productcoefficients))) -> exists pfc_value_euclidean_common_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_euclidean_common_productcoefficientscoefficientdiagonalentry. ff_h_pfp_euclidean_common_productcoefficientscoefficientdiagonalentry + S (pfc_value_euclidean_common_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_euclidean_common_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_productcoefficientscoefficient)) /\ exists ff_q_pfp_euclidean_common_productcoefficientscoefficientdiagonalentry. pfc_terms_code_euclidean_common_productcoefficientscoefficient = ff_q_pfp_euclidean_common_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_euclidean_common_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_productcoefficientscoefficient) + (pfc_value_euclidean_common_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_euclidean_common_productcoefficientscoefficientdiagonalterm pfc_left_euclidean_common_productcoefficientscoefficientdiagonalterm pfc_right_euclidean_common_productcoefficientscoefficientdiagonalterm. (((pfc_index_euclidean_common_productcoefficientscoefficientdiagonal)+pfc_complement_euclidean_common_productcoefficientscoefficientdiagonalterm=(pfc_index_euclidean_common_productcoefficients)) /\ ((((((exists pfa_gap_euclidean_common_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_euclidean_common_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_euclidean_common_productcoefficientscoefficientdiagonal) = (H)) /\ ((((exists ff_h_pfp_euclidean_common_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_euclidean_common_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_euclidean_common_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_euclidean_common_productcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_euclidean_common_productcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_euclidean_common_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_euclidean_common_productcoefficientscoefficientdiagonal)) * qc) + (pfc_left_euclidean_common_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_euclidean_common_productcoefficientscoefficientdiagonaltermleftoutside+(H)=(pfc_index_euclidean_common_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_euclidean_common_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_euclidean_common_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_euclidean_common_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_euclidean_common_productcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_euclidean_common_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_euclidean_common_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_euclidean_common_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_euclidean_common_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_euclidean_common_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_euclidean_common_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_euclidean_common_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_euclidean_common_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_euclidean_common_productcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_euclidean_common_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_euclidean_common_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_euclidean_common_productcoefficientscoefficientdiagonal)=pfc_left_euclidean_common_productcoefficientscoefficientdiagonalterm*pfc_right_euclidean_common_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_euclidean_common_productcoefficientscoefficientsum fs_v_pfc_euclidean_common_productcoefficientscoefficientsum. ((((exists fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_start. fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_euclidean_common_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_start. fs_u_pfc_euclidean_common_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_euclidean_common_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_euclidean_common_productcoefficientscoefficient) = S ((S (S (pfc_index_euclidean_common_productcoefficients))) * fs_v_pfc_euclidean_common_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_euclidean_common_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_euclidean_common_productcoefficients))) * fs_v_pfc_euclidean_common_productcoefficientscoefficientsum) + (pfc_natural_sum_euclidean_common_productcoefficientscoefficient))) /\ forall fs_i_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps = S (pfc_index_euclidean_common_productcoefficients)) -> exists fs_a_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps fs_r_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps fs_s_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_productcoefficientscoefficient)) /\ exists fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_euclidean_common_productcoefficientscoefficient = fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_productcoefficientscoefficient) + (fs_a_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_euclidean_common_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_productcoefficientscoefficientsum) + (fs_r_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_euclidean_common_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_productcoefficientscoefficientsum) + (fs_s_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps = fs_r_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps + fs_a_pfc_euclidean_common_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_euclidean_common_productcoefficientscoefficientresiduebound. pfa_gap_euclidean_common_productcoefficientscoefficientresiduebound + S (pfc_value_euclidean_common_productcoefficients) = (p)) /\ ((exists pfa_offset_left_euclidean_common_productcoefficientscoefficientresiduecongruence pfa_offset_right_euclidean_common_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_euclidean_common_productcoefficientscoefficient) + (p) * pfa_offset_left_euclidean_common_productcoefficientscoefficientresiduecongruence = (pfc_value_euclidean_common_productcoefficients) + (p) * pfa_offset_right_euclidean_common_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_euclidean_common_identity_left_bounded. (exists fom_gap_pfp_euclidean_common_identity_left_bounded_index_bound. fom_gap_pfp_euclidean_common_identity_left_bounded_index_bound + S (fom_index_pfp_euclidean_common_identity_left_bounded) = I) -> exists fom_value_pfp_euclidean_common_identity_left_bounded. ((((exists fom_beta_height_pfp_euclidean_common_identity_left_bounded_entry. fom_beta_height_pfp_euclidean_common_identity_left_bounded_entry + S (fom_value_pfp_euclidean_common_identity_left_bounded) = S ((S (fom_index_pfp_euclidean_common_identity_left_bounded)) * pc)) /\ exists fom_beta_quotient_pfp_euclidean_common_identity_left_bounded_entry. pb = fom_beta_quotient_pfp_euclidean_common_identity_left_bounded_entry * S ((S (fom_index_pfp_euclidean_common_identity_left_bounded)) * pc) + (fom_value_pfp_euclidean_common_identity_left_bounded))) /\ (exists fom_gap_pfp_euclidean_common_identity_left_bounded_value_bound. fom_gap_pfp_euclidean_common_identity_left_bounded_value_bound + S (fom_value_pfp_euclidean_common_identity_left_bounded) = p))) /\ (((forall fom_index_pfp_euclidean_common_identity_right_bounded. (exists fom_gap_pfp_euclidean_common_identity_right_bounded_index_bound. fom_gap_pfp_euclidean_common_identity_right_bounded_index_bound + S (fom_index_pfp_euclidean_common_identity_right_bounded) = N) -> exists fom_value_pfp_euclidean_common_identity_right_bounded. ((((exists fom_beta_height_pfp_euclidean_common_identity_right_bounded_entry. fom_beta_height_pfp_euclidean_common_identity_right_bounded_entry + S (fom_value_pfp_euclidean_common_identity_right_bounded) = S ((S (fom_index_pfp_euclidean_common_identity_right_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_euclidean_common_identity_right_bounded_entry. rb = fom_beta_quotient_pfp_euclidean_common_identity_right_bounded_entry * S ((S (fom_index_pfp_euclidean_common_identity_right_bounded)) * rc) + (fom_value_pfp_euclidean_common_identity_right_bounded))) /\ (exists fom_gap_pfp_euclidean_common_identity_right_bounded_value_bound. fom_gap_pfp_euclidean_common_identity_right_bounded_value_bound + S (fom_value_pfp_euclidean_common_identity_right_bounded) = p))) /\ (((forall fom_index_pfp_euclidean_common_identity_result_bounded. (exists fom_gap_pfp_euclidean_common_identity_result_bounded_index_bound. fom_gap_pfp_euclidean_common_identity_result_bounded_index_bound + S (fom_index_pfp_euclidean_common_identity_result_bounded) = L) -> exists fom_value_pfp_euclidean_common_identity_result_bounded. ((((exists fom_beta_height_pfp_euclidean_common_identity_result_bounded_entry. fom_beta_height_pfp_euclidean_common_identity_result_bounded_entry + S (fom_value_pfp_euclidean_common_identity_result_bounded) = S ((S (fom_index_pfp_euclidean_common_identity_result_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_euclidean_common_identity_result_bounded_entry. ab = fom_beta_quotient_pfp_euclidean_common_identity_result_bounded_entry * S ((S (fom_index_pfp_euclidean_common_identity_result_bounded)) * ac) + (fom_value_pfp_euclidean_common_identity_result_bounded))) /\ (exists fom_gap_pfp_euclidean_common_identity_result_bounded_value_bound. fom_gap_pfp_euclidean_common_identity_result_bounded_value_bound + S (fom_value_pfp_euclidean_common_identity_result_bounded) = p))) /\ ((exists pfaa_left_b_euclidean_common_identity pfaa_left_c_euclidean_common_identity pfaa_right_b_euclidean_common_identity pfaa_right_c_euclidean_common_identity pfaa_sum_b_euclidean_common_identity pfaa_sum_c_euclidean_common_identity pfaa_length_euclidean_common_identity. ((((forall pfrep_power_euclidean_common_identity_witness_common_left pfrep_left_euclidean_common_identity_witness_common_left pfrep_right_euclidean_common_identity_witness_common_left. ((exists pfrep_position_euclidean_common_identity_witness_common_leftfirst. ((pfrep_position_euclidean_common_identity_witness_common_leftfirst+S (pfrep_power_euclidean_common_identity_witness_common_left)=(I)) /\ ((((exists ff_h_pfp_euclidean_common_identity_witness_common_leftfirstentry. ff_h_pfp_euclidean_common_identity_witness_common_leftfirstentry + S (pfrep_left_euclidean_common_identity_witness_common_left) = S ((S (pfrep_position_euclidean_common_identity_witness_common_leftfirst)) * pc)) /\ exists ff_q_pfp_euclidean_common_identity_witness_common_leftfirstentry. pb = ff_q_pfp_euclidean_common_identity_witness_common_leftfirstentry * S ((S (pfrep_position_euclidean_common_identity_witness_common_leftfirst)) * pc) + (pfrep_left_euclidean_common_identity_witness_common_left)))))) \/ (((exists pfrep_gap_euclidean_common_identity_witness_common_leftfirstoutside. pfrep_gap_euclidean_common_identity_witness_common_leftfirstoutside+(I)=(pfrep_power_euclidean_common_identity_witness_common_left)) /\ (((pfrep_left_euclidean_common_identity_witness_common_left)=0))))) -> ((exists pfrep_position_euclidean_common_identity_witness_common_leftsecond. ((pfrep_position_euclidean_common_identity_witness_common_leftsecond+S (pfrep_power_euclidean_common_identity_witness_common_left)=(pfaa_length_euclidean_common_identity)) /\ ((((exists ff_h_pfp_euclidean_common_identity_witness_common_leftsecondentry. ff_h_pfp_euclidean_common_identity_witness_common_leftsecondentry + S (pfrep_right_euclidean_common_identity_witness_common_left) = S ((S (pfrep_position_euclidean_common_identity_witness_common_leftsecond)) * pfaa_left_c_euclidean_common_identity)) /\ exists ff_q_pfp_euclidean_common_identity_witness_common_leftsecondentry. pfaa_left_b_euclidean_common_identity = ff_q_pfp_euclidean_common_identity_witness_common_leftsecondentry * S ((S (pfrep_position_euclidean_common_identity_witness_common_leftsecond)) * pfaa_left_c_euclidean_common_identity) + (pfrep_right_euclidean_common_identity_witness_common_left)))))) \/ (((exists pfrep_gap_euclidean_common_identity_witness_common_leftsecondoutside. pfrep_gap_euclidean_common_identity_witness_common_leftsecondoutside+(pfaa_length_euclidean_common_identity)=(pfrep_power_euclidean_common_identity_witness_common_left)) /\ (((pfrep_right_euclidean_common_identity_witness_common_left)=0))))) -> pfrep_left_euclidean_common_identity_witness_common_left=pfrep_right_euclidean_common_identity_witness_common_left) /\ ((forall pfrep_power_euclidean_common_identity_witness_common_right pfrep_left_euclidean_common_identity_witness_common_right pfrep_right_euclidean_common_identity_witness_common_right. ((exists pfrep_position_euclidean_common_identity_witness_common_rightfirst. ((pfrep_position_euclidean_common_identity_witness_common_rightfirst+S (pfrep_power_euclidean_common_identity_witness_common_right)=(N)) /\ ((((exists ff_h_pfp_euclidean_common_identity_witness_common_rightfirstentry. ff_h_pfp_euclidean_common_identity_witness_common_rightfirstentry + S (pfrep_left_euclidean_common_identity_witness_common_right) = S ((S (pfrep_position_euclidean_common_identity_witness_common_rightfirst)) * rc)) /\ exists ff_q_pfp_euclidean_common_identity_witness_common_rightfirstentry. rb = ff_q_pfp_euclidean_common_identity_witness_common_rightfirstentry * S ((S (pfrep_position_euclidean_common_identity_witness_common_rightfirst)) * rc) + (pfrep_left_euclidean_common_identity_witness_common_right)))))) \/ (((exists pfrep_gap_euclidean_common_identity_witness_common_rightfirstoutside. pfrep_gap_euclidean_common_identity_witness_common_rightfirstoutside+(N)=(pfrep_power_euclidean_common_identity_witness_common_right)) /\ (((pfrep_left_euclidean_common_identity_witness_common_right)=0))))) -> ((exists pfrep_position_euclidean_common_identity_witness_common_rightsecond. ((pfrep_position_euclidean_common_identity_witness_common_rightsecond+S (pfrep_power_euclidean_common_identity_witness_common_right)=(pfaa_length_euclidean_common_identity)) /\ ((((exists ff_h_pfp_euclidean_common_identity_witness_common_rightsecondentry. ff_h_pfp_euclidean_common_identity_witness_common_rightsecondentry + S (pfrep_right_euclidean_common_identity_witness_common_right) = S ((S (pfrep_position_euclidean_common_identity_witness_common_rightsecond)) * pfaa_right_c_euclidean_common_identity)) /\ exists ff_q_pfp_euclidean_common_identity_witness_common_rightsecondentry. pfaa_right_b_euclidean_common_identity = ff_q_pfp_euclidean_common_identity_witness_common_rightsecondentry * S ((S (pfrep_position_euclidean_common_identity_witness_common_rightsecond)) * pfaa_right_c_euclidean_common_identity) + (pfrep_right_euclidean_common_identity_witness_common_right)))))) \/ (((exists pfrep_gap_euclidean_common_identity_witness_common_rightsecondoutside. pfrep_gap_euclidean_common_identity_witness_common_rightsecondoutside+(pfaa_length_euclidean_common_identity)=(pfrep_power_euclidean_common_identity_witness_common_right)) /\ (((pfrep_right_euclidean_common_identity_witness_common_right)=0))))) -> pfrep_left_euclidean_common_identity_witness_common_right=pfrep_right_euclidean_common_identity_witness_common_right)))) /\ (((forall pfp_index_euclidean_common_identity_witness_operation. (exists pfa_gap_euclidean_common_identity_witness_operationindex. pfa_gap_euclidean_common_identity_witness_operationindex + S (pfp_index_euclidean_common_identity_witness_operation) = (pfaa_length_euclidean_common_identity)) -> exists pfp_left_euclidean_common_identity_witness_operation pfp_right_euclidean_common_identity_witness_operation pfp_value_euclidean_common_identity_witness_operation. ((((exists ff_h_pfp_euclidean_common_identity_witness_operationleft. ff_h_pfp_euclidean_common_identity_witness_operationleft + S (pfp_left_euclidean_common_identity_witness_operation) = S ((S (pfp_index_euclidean_common_identity_witness_operation)) * pfaa_left_c_euclidean_common_identity)) /\ exists ff_q_pfp_euclidean_common_identity_witness_operationleft. pfaa_left_b_euclidean_common_identity = ff_q_pfp_euclidean_common_identity_witness_operationleft * S ((S (pfp_index_euclidean_common_identity_witness_operation)) * pfaa_left_c_euclidean_common_identity) + (pfp_left_euclidean_common_identity_witness_operation))) /\ (((((exists ff_h_pfp_euclidean_common_identity_witness_operationright. ff_h_pfp_euclidean_common_identity_witness_operationright + S (pfp_right_euclidean_common_identity_witness_operation) = S ((S (pfp_index_euclidean_common_identity_witness_operation)) * pfaa_right_c_euclidean_common_identity)) /\ exists ff_q_pfp_euclidean_common_identity_witness_operationright. pfaa_right_b_euclidean_common_identity = ff_q_pfp_euclidean_common_identity_witness_operationright * S ((S (pfp_index_euclidean_common_identity_witness_operation)) * pfaa_right_c_euclidean_common_identity) + (pfp_right_euclidean_common_identity_witness_operation))) /\ (((((exists ff_h_pfp_euclidean_common_identity_witness_operationtarget. ff_h_pfp_euclidean_common_identity_witness_operationtarget + S (pfp_value_euclidean_common_identity_witness_operation) = S ((S (pfp_index_euclidean_common_identity_witness_operation)) * pfaa_sum_c_euclidean_common_identity)) /\ exists ff_q_pfp_euclidean_common_identity_witness_operationtarget. pfaa_sum_b_euclidean_common_identity = ff_q_pfp_euclidean_common_identity_witness_operationtarget * S ((S (pfp_index_euclidean_common_identity_witness_operation)) * pfaa_sum_c_euclidean_common_identity) + (pfp_value_euclidean_common_identity_witness_operation))) /\ ((((exists pfa_gap_euclidean_common_identity_witness_operationoperationleft. pfa_gap_euclidean_common_identity_witness_operationoperationleft + S (pfp_left_euclidean_common_identity_witness_operation) = (p)) /\ (((exists pfa_gap_euclidean_common_identity_witness_operationoperationright. pfa_gap_euclidean_common_identity_witness_operationoperationright + S (pfp_right_euclidean_common_identity_witness_operation) = (p)) /\ ((((exists pfa_gap_euclidean_common_identity_witness_operationoperationresultbound. pfa_gap_euclidean_common_identity_witness_operationoperationresultbound + S (pfp_value_euclidean_common_identity_witness_operation) = (p)) /\ ((exists pfa_offset_left_euclidean_common_identity_witness_operationoperationresultcongruence pfa_offset_right_euclidean_common_identity_witness_operationoperationresultcongruence. ((pfp_left_euclidean_common_identity_witness_operation) + (pfp_right_euclidean_common_identity_witness_operation)) + (p) * pfa_offset_left_euclidean_common_identity_witness_operationoperationresultcongruence = (pfp_value_euclidean_common_identity_witness_operation) + (p) * pfa_offset_right_euclidean_common_identity_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_euclidean_common_identity_witness_output pfrep_left_euclidean_common_identity_witness_output pfrep_right_euclidean_common_identity_witness_output. ((exists pfrep_position_euclidean_common_identity_witness_outputfirst. ((pfrep_position_euclidean_common_identity_witness_outputfirst+S (pfrep_power_euclidean_common_identity_witness_output)=(pfaa_length_euclidean_common_identity)) /\ ((((exists ff_h_pfp_euclidean_common_identity_witness_outputfirstentry. ff_h_pfp_euclidean_common_identity_witness_outputfirstentry + S (pfrep_left_euclidean_common_identity_witness_output) = S ((S (pfrep_position_euclidean_common_identity_witness_outputfirst)) * pfaa_sum_c_euclidean_common_identity)) /\ exists ff_q_pfp_euclidean_common_identity_witness_outputfirstentry. pfaa_sum_b_euclidean_common_identity = ff_q_pfp_euclidean_common_identity_witness_outputfirstentry * S ((S (pfrep_position_euclidean_common_identity_witness_outputfirst)) * pfaa_sum_c_euclidean_common_identity) + (pfrep_left_euclidean_common_identity_witness_output)))))) \/ (((exists pfrep_gap_euclidean_common_identity_witness_outputfirstoutside. pfrep_gap_euclidean_common_identity_witness_outputfirstoutside+(pfaa_length_euclidean_common_identity)=(pfrep_power_euclidean_common_identity_witness_output)) /\ (((pfrep_left_euclidean_common_identity_witness_output)=0))))) -> ((exists pfrep_position_euclidean_common_identity_witness_outputsecond. ((pfrep_position_euclidean_common_identity_witness_outputsecond+S (pfrep_power_euclidean_common_identity_witness_output)=(L)) /\ ((((exists ff_h_pfp_euclidean_common_identity_witness_outputsecondentry. ff_h_pfp_euclidean_common_identity_witness_outputsecondentry + S (pfrep_right_euclidean_common_identity_witness_output) = S ((S (pfrep_position_euclidean_common_identity_witness_outputsecond)) * ac)) /\ exists ff_q_pfp_euclidean_common_identity_witness_outputsecondentry. ab = ff_q_pfp_euclidean_common_identity_witness_outputsecondentry * S ((S (pfrep_position_euclidean_common_identity_witness_outputsecond)) * ac) + (pfrep_right_euclidean_common_identity_witness_output)))))) \/ (((exists pfrep_gap_euclidean_common_identity_witness_outputsecondoutside. pfrep_gap_euclidean_common_identity_witness_outputsecondoutside+(L)=(pfrep_power_euclidean_common_identity_witness_output)) /\ (((pfrep_right_euclidean_common_identity_witness_output)=0))))) -> pfrep_left_euclidean_common_identity_witness_output=pfrep_right_euclidean_common_identity_witness_output))))))))))))) -> ((((((((forall fom_index_pfp_euclidean_common_source_left_canonical. (exists fom_gap_pfp_euclidean_common_source_left_canonical_index_bound. fom_gap_pfp_euclidean_common_source_left_canonical_index_bound + S (fom_index_pfp_euclidean_common_source_left_canonical) = L) -> exists fom_value_pfp_euclidean_common_source_left_canonical. ((((exists fom_beta_height_pfp_euclidean_common_source_left_canonical_entry. fom_beta_height_pfp_euclidean_common_source_left_canonical_entry + S (fom_value_pfp_euclidean_common_source_left_canonical) = S ((S (fom_index_pfp_euclidean_common_source_left_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_left_canonical_entry. ab = fom_beta_quotient_pfp_euclidean_common_source_left_canonical_entry * S ((S (fom_index_pfp_euclidean_common_source_left_canonical)) * ac) + (fom_value_pfp_euclidean_common_source_left_canonical))) /\ (exists fom_gap_pfp_euclidean_common_source_left_canonical_value_bound. fom_gap_pfp_euclidean_common_source_left_canonical_value_bound + S (fom_value_pfp_euclidean_common_source_left_canonical) = p))) /\ ((exists pfrd_qb_euclidean_common_source_left pfrd_qc_euclidean_common_source_left pfrd_qlen_euclidean_common_source_left pfrd_pb_euclidean_common_source_left pfrd_pc_euclidean_common_source_left pfrd_plen_euclidean_common_source_left. ((((forall fom_index_pfp_euclidean_common_source_left_productleft. (exists fom_gap_pfp_euclidean_common_source_left_productleft_index_bound. fom_gap_pfp_euclidean_common_source_left_productleft_index_bound + S (fom_index_pfp_euclidean_common_source_left_productleft) = pfrd_qlen_euclidean_common_source_left) -> exists fom_value_pfp_euclidean_common_source_left_productleft. ((((exists fom_beta_height_pfp_euclidean_common_source_left_productleft_entry. fom_beta_height_pfp_euclidean_common_source_left_productleft_entry + S (fom_value_pfp_euclidean_common_source_left_productleft) = S ((S (fom_index_pfp_euclidean_common_source_left_productleft)) * pfrd_qc_euclidean_common_source_left)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_left_productleft_entry. pfrd_qb_euclidean_common_source_left = fom_beta_quotient_pfp_euclidean_common_source_left_productleft_entry * S ((S (fom_index_pfp_euclidean_common_source_left_productleft)) * pfrd_qc_euclidean_common_source_left) + (fom_value_pfp_euclidean_common_source_left_productleft))) /\ (exists fom_gap_pfp_euclidean_common_source_left_productleft_value_bound. fom_gap_pfp_euclidean_common_source_left_productleft_value_bound + S (fom_value_pfp_euclidean_common_source_left_productleft) = p))) /\ (((forall fom_index_pfp_euclidean_common_source_left_productright. (exists fom_gap_pfp_euclidean_common_source_left_productright_index_bound. fom_gap_pfp_euclidean_common_source_left_productright_index_bound + S (fom_index_pfp_euclidean_common_source_left_productright) = J) -> exists fom_value_pfp_euclidean_common_source_left_productright. ((((exists fom_beta_height_pfp_euclidean_common_source_left_productright_entry. fom_beta_height_pfp_euclidean_common_source_left_productright_entry + S (fom_value_pfp_euclidean_common_source_left_productright) = S ((S (fom_index_pfp_euclidean_common_source_left_productright)) * dc)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_left_productright_entry. db = fom_beta_quotient_pfp_euclidean_common_source_left_productright_entry * S ((S (fom_index_pfp_euclidean_common_source_left_productright)) * dc) + (fom_value_pfp_euclidean_common_source_left_productright))) /\ (exists fom_gap_pfp_euclidean_common_source_left_productright_value_bound. fom_gap_pfp_euclidean_common_source_left_productright_value_bound + S (fom_value_pfp_euclidean_common_source_left_productright) = p))) /\ (((((((pfrd_qlen_euclidean_common_source_left)=0 \/ (J)=0) /\ (((pfrd_plen_euclidean_common_source_left)=0)))) \/ (((~((pfrd_qlen_euclidean_common_source_left)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_euclidean_common_source_left)+(J)=S (pfrd_plen_euclidean_common_source_left)))))))) /\ ((forall pfc_index_euclidean_common_source_left_productcoefficients. (exists pfa_gap_euclidean_common_source_left_productcoefficientsbound. pfa_gap_euclidean_common_source_left_productcoefficientsbound + S (pfc_index_euclidean_common_source_left_productcoefficients) = (pfrd_plen_euclidean_common_source_left)) -> exists pfc_value_euclidean_common_source_left_productcoefficients. ((((exists ff_h_pfp_euclidean_common_source_left_productcoefficientsentry. ff_h_pfp_euclidean_common_source_left_productcoefficientsentry + S (pfc_value_euclidean_common_source_left_productcoefficients) = S ((S (pfc_index_euclidean_common_source_left_productcoefficients)) * pfrd_pc_euclidean_common_source_left)) /\ exists ff_q_pfp_euclidean_common_source_left_productcoefficientsentry. pfrd_pb_euclidean_common_source_left = ff_q_pfp_euclidean_common_source_left_productcoefficientsentry * S ((S (pfc_index_euclidean_common_source_left_productcoefficients)) * pfrd_pc_euclidean_common_source_left) + (pfc_value_euclidean_common_source_left_productcoefficients))) /\ ((exists pfc_terms_code_euclidean_common_source_left_productcoefficientscoefficient pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient pfc_natural_sum_euclidean_common_source_left_productcoefficientscoefficient. ((forall pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonalbound. pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_euclidean_common_source_left_productcoefficients))) -> exists pfc_value_euclidean_common_source_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_euclidean_common_source_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_euclidean_common_source_left_productcoefficientscoefficient = ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient) + (pfc_value_euclidean_common_source_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)+pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm=(pfc_index_euclidean_common_source_left_productcoefficients)) /\ ((((((exists pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal) = (pfrd_qlen_euclidean_common_source_left)) /\ ((((exists ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_source_left)) /\ exists ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_euclidean_common_source_left = ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_source_left) + (pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_euclidean_common_source_left)=(pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_euclidean_common_source_left_productcoefficientscoefficientdiagonal)=pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm*pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_euclidean_common_source_left_productcoefficientscoefficient) = S ((S (S (pfc_index_euclidean_common_source_left_productcoefficients))) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_euclidean_common_source_left_productcoefficients))) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum) + (pfc_natural_sum_euclidean_common_source_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_euclidean_common_source_left_productcoefficients)) -> exists fs_a_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_euclidean_common_source_left_productcoefficientscoefficient = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient) + (fs_a_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum) + (fs_r_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum) + (fs_s_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_euclidean_common_source_left_productcoefficientscoefficientresiduebound. pfa_gap_euclidean_common_source_left_productcoefficientscoefficientresiduebound + S (pfc_value_euclidean_common_source_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_euclidean_common_source_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_euclidean_common_source_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_euclidean_common_source_left_productcoefficientscoefficient) + (p) * pfa_offset_left_euclidean_common_source_left_productcoefficientscoefficientresiduecongruence = (pfc_value_euclidean_common_source_left_productcoefficients) + (p) * pfa_offset_right_euclidean_common_source_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_euclidean_common_source_left_target pfrep_left_euclidean_common_source_left_target pfrep_right_euclidean_common_source_left_target. ((exists pfrep_position_euclidean_common_source_left_targetfirst. ((pfrep_position_euclidean_common_source_left_targetfirst+S (pfrep_power_euclidean_common_source_left_target)=(pfrd_plen_euclidean_common_source_left)) /\ ((((exists ff_h_pfp_euclidean_common_source_left_targetfirstentry. ff_h_pfp_euclidean_common_source_left_targetfirstentry + S (pfrep_left_euclidean_common_source_left_target) = S ((S (pfrep_position_euclidean_common_source_left_targetfirst)) * pfrd_pc_euclidean_common_source_left)) /\ exists ff_q_pfp_euclidean_common_source_left_targetfirstentry. pfrd_pb_euclidean_common_source_left = ff_q_pfp_euclidean_common_source_left_targetfirstentry * S ((S (pfrep_position_euclidean_common_source_left_targetfirst)) * pfrd_pc_euclidean_common_source_left) + (pfrep_left_euclidean_common_source_left_target)))))) \/ (((exists pfrep_gap_euclidean_common_source_left_targetfirstoutside. pfrep_gap_euclidean_common_source_left_targetfirstoutside+(pfrd_plen_euclidean_common_source_left)=(pfrep_power_euclidean_common_source_left_target)) /\ (((pfrep_left_euclidean_common_source_left_target)=0))))) -> ((exists pfrep_position_euclidean_common_source_left_targetsecond. ((pfrep_position_euclidean_common_source_left_targetsecond+S (pfrep_power_euclidean_common_source_left_target)=(L)) /\ ((((exists ff_h_pfp_euclidean_common_source_left_targetsecondentry. ff_h_pfp_euclidean_common_source_left_targetsecondentry + S (pfrep_right_euclidean_common_source_left_target) = S ((S (pfrep_position_euclidean_common_source_left_targetsecond)) * ac)) /\ exists ff_q_pfp_euclidean_common_source_left_targetsecondentry. ab = ff_q_pfp_euclidean_common_source_left_targetsecondentry * S ((S (pfrep_position_euclidean_common_source_left_targetsecond)) * ac) + (pfrep_right_euclidean_common_source_left_target)))))) \/ (((exists pfrep_gap_euclidean_common_source_left_targetsecondoutside. pfrep_gap_euclidean_common_source_left_targetsecondoutside+(L)=(pfrep_power_euclidean_common_source_left_target)) /\ (((pfrep_right_euclidean_common_source_left_target)=0))))) -> pfrep_left_euclidean_common_source_left_target=pfrep_right_euclidean_common_source_left_target))))))) /\ ((((forall fom_index_pfp_euclidean_common_source_right_canonical. (exists fom_gap_pfp_euclidean_common_source_right_canonical_index_bound. fom_gap_pfp_euclidean_common_source_right_canonical_index_bound + S (fom_index_pfp_euclidean_common_source_right_canonical) = M) -> exists fom_value_pfp_euclidean_common_source_right_canonical. ((((exists fom_beta_height_pfp_euclidean_common_source_right_canonical_entry. fom_beta_height_pfp_euclidean_common_source_right_canonical_entry + S (fom_value_pfp_euclidean_common_source_right_canonical) = S ((S (fom_index_pfp_euclidean_common_source_right_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_right_canonical_entry. bb = fom_beta_quotient_pfp_euclidean_common_source_right_canonical_entry * S ((S (fom_index_pfp_euclidean_common_source_right_canonical)) * bc) + (fom_value_pfp_euclidean_common_source_right_canonical))) /\ (exists fom_gap_pfp_euclidean_common_source_right_canonical_value_bound. fom_gap_pfp_euclidean_common_source_right_canonical_value_bound + S (fom_value_pfp_euclidean_common_source_right_canonical) = p))) /\ ((exists pfrd_qb_euclidean_common_source_right pfrd_qc_euclidean_common_source_right pfrd_qlen_euclidean_common_source_right pfrd_pb_euclidean_common_source_right pfrd_pc_euclidean_common_source_right pfrd_plen_euclidean_common_source_right. ((((forall fom_index_pfp_euclidean_common_source_right_productleft. (exists fom_gap_pfp_euclidean_common_source_right_productleft_index_bound. fom_gap_pfp_euclidean_common_source_right_productleft_index_bound + S (fom_index_pfp_euclidean_common_source_right_productleft) = pfrd_qlen_euclidean_common_source_right) -> exists fom_value_pfp_euclidean_common_source_right_productleft. ((((exists fom_beta_height_pfp_euclidean_common_source_right_productleft_entry. fom_beta_height_pfp_euclidean_common_source_right_productleft_entry + S (fom_value_pfp_euclidean_common_source_right_productleft) = S ((S (fom_index_pfp_euclidean_common_source_right_productleft)) * pfrd_qc_euclidean_common_source_right)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_right_productleft_entry. pfrd_qb_euclidean_common_source_right = fom_beta_quotient_pfp_euclidean_common_source_right_productleft_entry * S ((S (fom_index_pfp_euclidean_common_source_right_productleft)) * pfrd_qc_euclidean_common_source_right) + (fom_value_pfp_euclidean_common_source_right_productleft))) /\ (exists fom_gap_pfp_euclidean_common_source_right_productleft_value_bound. fom_gap_pfp_euclidean_common_source_right_productleft_value_bound + S (fom_value_pfp_euclidean_common_source_right_productleft) = p))) /\ (((forall fom_index_pfp_euclidean_common_source_right_productright. (exists fom_gap_pfp_euclidean_common_source_right_productright_index_bound. fom_gap_pfp_euclidean_common_source_right_productright_index_bound + S (fom_index_pfp_euclidean_common_source_right_productright) = J) -> exists fom_value_pfp_euclidean_common_source_right_productright. ((((exists fom_beta_height_pfp_euclidean_common_source_right_productright_entry. fom_beta_height_pfp_euclidean_common_source_right_productright_entry + S (fom_value_pfp_euclidean_common_source_right_productright) = S ((S (fom_index_pfp_euclidean_common_source_right_productright)) * dc)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_right_productright_entry. db = fom_beta_quotient_pfp_euclidean_common_source_right_productright_entry * S ((S (fom_index_pfp_euclidean_common_source_right_productright)) * dc) + (fom_value_pfp_euclidean_common_source_right_productright))) /\ (exists fom_gap_pfp_euclidean_common_source_right_productright_value_bound. fom_gap_pfp_euclidean_common_source_right_productright_value_bound + S (fom_value_pfp_euclidean_common_source_right_productright) = p))) /\ (((((((pfrd_qlen_euclidean_common_source_right)=0 \/ (J)=0) /\ (((pfrd_plen_euclidean_common_source_right)=0)))) \/ (((~((pfrd_qlen_euclidean_common_source_right)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_euclidean_common_source_right)+(J)=S (pfrd_plen_euclidean_common_source_right)))))))) /\ ((forall pfc_index_euclidean_common_source_right_productcoefficients. (exists pfa_gap_euclidean_common_source_right_productcoefficientsbound. pfa_gap_euclidean_common_source_right_productcoefficientsbound + S (pfc_index_euclidean_common_source_right_productcoefficients) = (pfrd_plen_euclidean_common_source_right)) -> exists pfc_value_euclidean_common_source_right_productcoefficients. ((((exists ff_h_pfp_euclidean_common_source_right_productcoefficientsentry. ff_h_pfp_euclidean_common_source_right_productcoefficientsentry + S (pfc_value_euclidean_common_source_right_productcoefficients) = S ((S (pfc_index_euclidean_common_source_right_productcoefficients)) * pfrd_pc_euclidean_common_source_right)) /\ exists ff_q_pfp_euclidean_common_source_right_productcoefficientsentry. pfrd_pb_euclidean_common_source_right = ff_q_pfp_euclidean_common_source_right_productcoefficientsentry * S ((S (pfc_index_euclidean_common_source_right_productcoefficients)) * pfrd_pc_euclidean_common_source_right) + (pfc_value_euclidean_common_source_right_productcoefficients))) /\ ((exists pfc_terms_code_euclidean_common_source_right_productcoefficientscoefficient pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient pfc_natural_sum_euclidean_common_source_right_productcoefficientscoefficient. ((forall pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonalbound. pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_euclidean_common_source_right_productcoefficients))) -> exists pfc_value_euclidean_common_source_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_euclidean_common_source_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_euclidean_common_source_right_productcoefficientscoefficient = ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient) + (pfc_value_euclidean_common_source_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)+pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm=(pfc_index_euclidean_common_source_right_productcoefficients)) /\ ((((((exists pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal) = (pfrd_qlen_euclidean_common_source_right)) /\ ((((exists ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_source_right)) /\ exists ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_euclidean_common_source_right = ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_source_right) + (pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_euclidean_common_source_right)=(pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_euclidean_common_source_right_productcoefficientscoefficientdiagonal)=pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm*pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_euclidean_common_source_right_productcoefficientscoefficient) = S ((S (S (pfc_index_euclidean_common_source_right_productcoefficients))) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_euclidean_common_source_right_productcoefficients))) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum) + (pfc_natural_sum_euclidean_common_source_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_euclidean_common_source_right_productcoefficients)) -> exists fs_a_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_euclidean_common_source_right_productcoefficientscoefficient = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient) + (fs_a_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum) + (fs_r_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum) + (fs_s_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_euclidean_common_source_right_productcoefficientscoefficientresiduebound. pfa_gap_euclidean_common_source_right_productcoefficientscoefficientresiduebound + S (pfc_value_euclidean_common_source_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_euclidean_common_source_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_euclidean_common_source_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_euclidean_common_source_right_productcoefficientscoefficient) + (p) * pfa_offset_left_euclidean_common_source_right_productcoefficientscoefficientresiduecongruence = (pfc_value_euclidean_common_source_right_productcoefficients) + (p) * pfa_offset_right_euclidean_common_source_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_euclidean_common_source_right_target pfrep_left_euclidean_common_source_right_target pfrep_right_euclidean_common_source_right_target. ((exists pfrep_position_euclidean_common_source_right_targetfirst. ((pfrep_position_euclidean_common_source_right_targetfirst+S (pfrep_power_euclidean_common_source_right_target)=(pfrd_plen_euclidean_common_source_right)) /\ ((((exists ff_h_pfp_euclidean_common_source_right_targetfirstentry. ff_h_pfp_euclidean_common_source_right_targetfirstentry + S (pfrep_left_euclidean_common_source_right_target) = S ((S (pfrep_position_euclidean_common_source_right_targetfirst)) * pfrd_pc_euclidean_common_source_right)) /\ exists ff_q_pfp_euclidean_common_source_right_targetfirstentry. pfrd_pb_euclidean_common_source_right = ff_q_pfp_euclidean_common_source_right_targetfirstentry * S ((S (pfrep_position_euclidean_common_source_right_targetfirst)) * pfrd_pc_euclidean_common_source_right) + (pfrep_left_euclidean_common_source_right_target)))))) \/ (((exists pfrep_gap_euclidean_common_source_right_targetfirstoutside. pfrep_gap_euclidean_common_source_right_targetfirstoutside+(pfrd_plen_euclidean_common_source_right)=(pfrep_power_euclidean_common_source_right_target)) /\ (((pfrep_left_euclidean_common_source_right_target)=0))))) -> ((exists pfrep_position_euclidean_common_source_right_targetsecond. ((pfrep_position_euclidean_common_source_right_targetsecond+S (pfrep_power_euclidean_common_source_right_target)=(M)) /\ ((((exists ff_h_pfp_euclidean_common_source_right_targetsecondentry. ff_h_pfp_euclidean_common_source_right_targetsecondentry + S (pfrep_right_euclidean_common_source_right_target) = S ((S (pfrep_position_euclidean_common_source_right_targetsecond)) * bc)) /\ exists ff_q_pfp_euclidean_common_source_right_targetsecondentry. bb = ff_q_pfp_euclidean_common_source_right_targetsecondentry * S ((S (pfrep_position_euclidean_common_source_right_targetsecond)) * bc) + (pfrep_right_euclidean_common_source_right_target)))))) \/ (((exists pfrep_gap_euclidean_common_source_right_targetsecondoutside. pfrep_gap_euclidean_common_source_right_targetsecondoutside+(M)=(pfrep_power_euclidean_common_source_right_target)) /\ (((pfrep_right_euclidean_common_source_right_target)=0))))) -> pfrep_left_euclidean_common_source_right_target=pfrep_right_euclidean_common_source_right_target)))))))))) -> (((((forall fom_index_pfp_euclidean_common_target_left_canonical. (exists fom_gap_pfp_euclidean_common_target_left_canonical_index_bound. fom_gap_pfp_euclidean_common_target_left_canonical_index_bound + S (fom_index_pfp_euclidean_common_target_left_canonical) = M) -> exists fom_value_pfp_euclidean_common_target_left_canonical. ((((exists fom_beta_height_pfp_euclidean_common_target_left_canonical_entry. fom_beta_height_pfp_euclidean_common_target_left_canonical_entry + S (fom_value_pfp_euclidean_common_target_left_canonical) = S ((S (fom_index_pfp_euclidean_common_target_left_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_left_canonical_entry. bb = fom_beta_quotient_pfp_euclidean_common_target_left_canonical_entry * S ((S (fom_index_pfp_euclidean_common_target_left_canonical)) * bc) + (fom_value_pfp_euclidean_common_target_left_canonical))) /\ (exists fom_gap_pfp_euclidean_common_target_left_canonical_value_bound. fom_gap_pfp_euclidean_common_target_left_canonical_value_bound + S (fom_value_pfp_euclidean_common_target_left_canonical) = p))) /\ ((exists pfrd_qb_euclidean_common_target_left pfrd_qc_euclidean_common_target_left pfrd_qlen_euclidean_common_target_left pfrd_pb_euclidean_common_target_left pfrd_pc_euclidean_common_target_left pfrd_plen_euclidean_common_target_left. ((((forall fom_index_pfp_euclidean_common_target_left_productleft. (exists fom_gap_pfp_euclidean_common_target_left_productleft_index_bound. fom_gap_pfp_euclidean_common_target_left_productleft_index_bound + S (fom_index_pfp_euclidean_common_target_left_productleft) = pfrd_qlen_euclidean_common_target_left) -> exists fom_value_pfp_euclidean_common_target_left_productleft. ((((exists fom_beta_height_pfp_euclidean_common_target_left_productleft_entry. fom_beta_height_pfp_euclidean_common_target_left_productleft_entry + S (fom_value_pfp_euclidean_common_target_left_productleft) = S ((S (fom_index_pfp_euclidean_common_target_left_productleft)) * pfrd_qc_euclidean_common_target_left)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_left_productleft_entry. pfrd_qb_euclidean_common_target_left = fom_beta_quotient_pfp_euclidean_common_target_left_productleft_entry * S ((S (fom_index_pfp_euclidean_common_target_left_productleft)) * pfrd_qc_euclidean_common_target_left) + (fom_value_pfp_euclidean_common_target_left_productleft))) /\ (exists fom_gap_pfp_euclidean_common_target_left_productleft_value_bound. fom_gap_pfp_euclidean_common_target_left_productleft_value_bound + S (fom_value_pfp_euclidean_common_target_left_productleft) = p))) /\ (((forall fom_index_pfp_euclidean_common_target_left_productright. (exists fom_gap_pfp_euclidean_common_target_left_productright_index_bound. fom_gap_pfp_euclidean_common_target_left_productright_index_bound + S (fom_index_pfp_euclidean_common_target_left_productright) = J) -> exists fom_value_pfp_euclidean_common_target_left_productright. ((((exists fom_beta_height_pfp_euclidean_common_target_left_productright_entry. fom_beta_height_pfp_euclidean_common_target_left_productright_entry + S (fom_value_pfp_euclidean_common_target_left_productright) = S ((S (fom_index_pfp_euclidean_common_target_left_productright)) * dc)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_left_productright_entry. db = fom_beta_quotient_pfp_euclidean_common_target_left_productright_entry * S ((S (fom_index_pfp_euclidean_common_target_left_productright)) * dc) + (fom_value_pfp_euclidean_common_target_left_productright))) /\ (exists fom_gap_pfp_euclidean_common_target_left_productright_value_bound. fom_gap_pfp_euclidean_common_target_left_productright_value_bound + S (fom_value_pfp_euclidean_common_target_left_productright) = p))) /\ (((((((pfrd_qlen_euclidean_common_target_left)=0 \/ (J)=0) /\ (((pfrd_plen_euclidean_common_target_left)=0)))) \/ (((~((pfrd_qlen_euclidean_common_target_left)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_euclidean_common_target_left)+(J)=S (pfrd_plen_euclidean_common_target_left)))))))) /\ ((forall pfc_index_euclidean_common_target_left_productcoefficients. (exists pfa_gap_euclidean_common_target_left_productcoefficientsbound. pfa_gap_euclidean_common_target_left_productcoefficientsbound + S (pfc_index_euclidean_common_target_left_productcoefficients) = (pfrd_plen_euclidean_common_target_left)) -> exists pfc_value_euclidean_common_target_left_productcoefficients. ((((exists ff_h_pfp_euclidean_common_target_left_productcoefficientsentry. ff_h_pfp_euclidean_common_target_left_productcoefficientsentry + S (pfc_value_euclidean_common_target_left_productcoefficients) = S ((S (pfc_index_euclidean_common_target_left_productcoefficients)) * pfrd_pc_euclidean_common_target_left)) /\ exists ff_q_pfp_euclidean_common_target_left_productcoefficientsentry. pfrd_pb_euclidean_common_target_left = ff_q_pfp_euclidean_common_target_left_productcoefficientsentry * S ((S (pfc_index_euclidean_common_target_left_productcoefficients)) * pfrd_pc_euclidean_common_target_left) + (pfc_value_euclidean_common_target_left_productcoefficients))) /\ ((exists pfc_terms_code_euclidean_common_target_left_productcoefficientscoefficient pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient pfc_natural_sum_euclidean_common_target_left_productcoefficientscoefficient. ((forall pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonalbound. pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_euclidean_common_target_left_productcoefficients))) -> exists pfc_value_euclidean_common_target_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_euclidean_common_target_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_euclidean_common_target_left_productcoefficientscoefficient = ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient) + (pfc_value_euclidean_common_target_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)+pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm=(pfc_index_euclidean_common_target_left_productcoefficients)) /\ ((((((exists pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal) = (pfrd_qlen_euclidean_common_target_left)) /\ ((((exists ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_target_left)) /\ exists ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_euclidean_common_target_left = ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_target_left) + (pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_euclidean_common_target_left)=(pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_euclidean_common_target_left_productcoefficientscoefficientdiagonal)=pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm*pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_euclidean_common_target_left_productcoefficientscoefficient) = S ((S (S (pfc_index_euclidean_common_target_left_productcoefficients))) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_euclidean_common_target_left_productcoefficients))) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum) + (pfc_natural_sum_euclidean_common_target_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_euclidean_common_target_left_productcoefficients)) -> exists fs_a_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_euclidean_common_target_left_productcoefficientscoefficient = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient) + (fs_a_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum) + (fs_r_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum) + (fs_s_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_euclidean_common_target_left_productcoefficientscoefficientresiduebound. pfa_gap_euclidean_common_target_left_productcoefficientscoefficientresiduebound + S (pfc_value_euclidean_common_target_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_euclidean_common_target_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_euclidean_common_target_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_euclidean_common_target_left_productcoefficientscoefficient) + (p) * pfa_offset_left_euclidean_common_target_left_productcoefficientscoefficientresiduecongruence = (pfc_value_euclidean_common_target_left_productcoefficients) + (p) * pfa_offset_right_euclidean_common_target_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_euclidean_common_target_left_target pfrep_left_euclidean_common_target_left_target pfrep_right_euclidean_common_target_left_target. ((exists pfrep_position_euclidean_common_target_left_targetfirst. ((pfrep_position_euclidean_common_target_left_targetfirst+S (pfrep_power_euclidean_common_target_left_target)=(pfrd_plen_euclidean_common_target_left)) /\ ((((exists ff_h_pfp_euclidean_common_target_left_targetfirstentry. ff_h_pfp_euclidean_common_target_left_targetfirstentry + S (pfrep_left_euclidean_common_target_left_target) = S ((S (pfrep_position_euclidean_common_target_left_targetfirst)) * pfrd_pc_euclidean_common_target_left)) /\ exists ff_q_pfp_euclidean_common_target_left_targetfirstentry. pfrd_pb_euclidean_common_target_left = ff_q_pfp_euclidean_common_target_left_targetfirstentry * S ((S (pfrep_position_euclidean_common_target_left_targetfirst)) * pfrd_pc_euclidean_common_target_left) + (pfrep_left_euclidean_common_target_left_target)))))) \/ (((exists pfrep_gap_euclidean_common_target_left_targetfirstoutside. pfrep_gap_euclidean_common_target_left_targetfirstoutside+(pfrd_plen_euclidean_common_target_left)=(pfrep_power_euclidean_common_target_left_target)) /\ (((pfrep_left_euclidean_common_target_left_target)=0))))) -> ((exists pfrep_position_euclidean_common_target_left_targetsecond. ((pfrep_position_euclidean_common_target_left_targetsecond+S (pfrep_power_euclidean_common_target_left_target)=(M)) /\ ((((exists ff_h_pfp_euclidean_common_target_left_targetsecondentry. ff_h_pfp_euclidean_common_target_left_targetsecondentry + S (pfrep_right_euclidean_common_target_left_target) = S ((S (pfrep_position_euclidean_common_target_left_targetsecond)) * bc)) /\ exists ff_q_pfp_euclidean_common_target_left_targetsecondentry. bb = ff_q_pfp_euclidean_common_target_left_targetsecondentry * S ((S (pfrep_position_euclidean_common_target_left_targetsecond)) * bc) + (pfrep_right_euclidean_common_target_left_target)))))) \/ (((exists pfrep_gap_euclidean_common_target_left_targetsecondoutside. pfrep_gap_euclidean_common_target_left_targetsecondoutside+(M)=(pfrep_power_euclidean_common_target_left_target)) /\ (((pfrep_right_euclidean_common_target_left_target)=0))))) -> pfrep_left_euclidean_common_target_left_target=pfrep_right_euclidean_common_target_left_target))))))) /\ ((((forall fom_index_pfp_euclidean_common_target_right_canonical. (exists fom_gap_pfp_euclidean_common_target_right_canonical_index_bound. fom_gap_pfp_euclidean_common_target_right_canonical_index_bound + S (fom_index_pfp_euclidean_common_target_right_canonical) = N) -> exists fom_value_pfp_euclidean_common_target_right_canonical. ((((exists fom_beta_height_pfp_euclidean_common_target_right_canonical_entry. fom_beta_height_pfp_euclidean_common_target_right_canonical_entry + S (fom_value_pfp_euclidean_common_target_right_canonical) = S ((S (fom_index_pfp_euclidean_common_target_right_canonical)) * rc)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_right_canonical_entry. rb = fom_beta_quotient_pfp_euclidean_common_target_right_canonical_entry * S ((S (fom_index_pfp_euclidean_common_target_right_canonical)) * rc) + (fom_value_pfp_euclidean_common_target_right_canonical))) /\ (exists fom_gap_pfp_euclidean_common_target_right_canonical_value_bound. fom_gap_pfp_euclidean_common_target_right_canonical_value_bound + S (fom_value_pfp_euclidean_common_target_right_canonical) = p))) /\ ((exists pfrd_qb_euclidean_common_target_right pfrd_qc_euclidean_common_target_right pfrd_qlen_euclidean_common_target_right pfrd_pb_euclidean_common_target_right pfrd_pc_euclidean_common_target_right pfrd_plen_euclidean_common_target_right. ((((forall fom_index_pfp_euclidean_common_target_right_productleft. (exists fom_gap_pfp_euclidean_common_target_right_productleft_index_bound. fom_gap_pfp_euclidean_common_target_right_productleft_index_bound + S (fom_index_pfp_euclidean_common_target_right_productleft) = pfrd_qlen_euclidean_common_target_right) -> exists fom_value_pfp_euclidean_common_target_right_productleft. ((((exists fom_beta_height_pfp_euclidean_common_target_right_productleft_entry. fom_beta_height_pfp_euclidean_common_target_right_productleft_entry + S (fom_value_pfp_euclidean_common_target_right_productleft) = S ((S (fom_index_pfp_euclidean_common_target_right_productleft)) * pfrd_qc_euclidean_common_target_right)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_right_productleft_entry. pfrd_qb_euclidean_common_target_right = fom_beta_quotient_pfp_euclidean_common_target_right_productleft_entry * S ((S (fom_index_pfp_euclidean_common_target_right_productleft)) * pfrd_qc_euclidean_common_target_right) + (fom_value_pfp_euclidean_common_target_right_productleft))) /\ (exists fom_gap_pfp_euclidean_common_target_right_productleft_value_bound. fom_gap_pfp_euclidean_common_target_right_productleft_value_bound + S (fom_value_pfp_euclidean_common_target_right_productleft) = p))) /\ (((forall fom_index_pfp_euclidean_common_target_right_productright. (exists fom_gap_pfp_euclidean_common_target_right_productright_index_bound. fom_gap_pfp_euclidean_common_target_right_productright_index_bound + S (fom_index_pfp_euclidean_common_target_right_productright) = J) -> exists fom_value_pfp_euclidean_common_target_right_productright. ((((exists fom_beta_height_pfp_euclidean_common_target_right_productright_entry. fom_beta_height_pfp_euclidean_common_target_right_productright_entry + S (fom_value_pfp_euclidean_common_target_right_productright) = S ((S (fom_index_pfp_euclidean_common_target_right_productright)) * dc)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_right_productright_entry. db = fom_beta_quotient_pfp_euclidean_common_target_right_productright_entry * S ((S (fom_index_pfp_euclidean_common_target_right_productright)) * dc) + (fom_value_pfp_euclidean_common_target_right_productright))) /\ (exists fom_gap_pfp_euclidean_common_target_right_productright_value_bound. fom_gap_pfp_euclidean_common_target_right_productright_value_bound + S (fom_value_pfp_euclidean_common_target_right_productright) = p))) /\ (((((((pfrd_qlen_euclidean_common_target_right)=0 \/ (J)=0) /\ (((pfrd_plen_euclidean_common_target_right)=0)))) \/ (((~((pfrd_qlen_euclidean_common_target_right)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_euclidean_common_target_right)+(J)=S (pfrd_plen_euclidean_common_target_right)))))))) /\ ((forall pfc_index_euclidean_common_target_right_productcoefficients. (exists pfa_gap_euclidean_common_target_right_productcoefficientsbound. pfa_gap_euclidean_common_target_right_productcoefficientsbound + S (pfc_index_euclidean_common_target_right_productcoefficients) = (pfrd_plen_euclidean_common_target_right)) -> exists pfc_value_euclidean_common_target_right_productcoefficients. ((((exists ff_h_pfp_euclidean_common_target_right_productcoefficientsentry. ff_h_pfp_euclidean_common_target_right_productcoefficientsentry + S (pfc_value_euclidean_common_target_right_productcoefficients) = S ((S (pfc_index_euclidean_common_target_right_productcoefficients)) * pfrd_pc_euclidean_common_target_right)) /\ exists ff_q_pfp_euclidean_common_target_right_productcoefficientsentry. pfrd_pb_euclidean_common_target_right = ff_q_pfp_euclidean_common_target_right_productcoefficientsentry * S ((S (pfc_index_euclidean_common_target_right_productcoefficients)) * pfrd_pc_euclidean_common_target_right) + (pfc_value_euclidean_common_target_right_productcoefficients))) /\ ((exists pfc_terms_code_euclidean_common_target_right_productcoefficientscoefficient pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient pfc_natural_sum_euclidean_common_target_right_productcoefficientscoefficient. ((forall pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonalbound. pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_euclidean_common_target_right_productcoefficients))) -> exists pfc_value_euclidean_common_target_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_euclidean_common_target_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_euclidean_common_target_right_productcoefficientscoefficient = ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient) + (pfc_value_euclidean_common_target_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)+pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm=(pfc_index_euclidean_common_target_right_productcoefficients)) /\ ((((((exists pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal) = (pfrd_qlen_euclidean_common_target_right)) /\ ((((exists ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_target_right)) /\ exists ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_euclidean_common_target_right = ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_target_right) + (pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_euclidean_common_target_right)=(pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_euclidean_common_target_right_productcoefficientscoefficientdiagonal)=pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm*pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_euclidean_common_target_right_productcoefficientscoefficient) = S ((S (S (pfc_index_euclidean_common_target_right_productcoefficients))) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_euclidean_common_target_right_productcoefficients))) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum) + (pfc_natural_sum_euclidean_common_target_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_euclidean_common_target_right_productcoefficients)) -> exists fs_a_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_euclidean_common_target_right_productcoefficientscoefficient = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient) + (fs_a_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum) + (fs_r_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum) + (fs_s_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_euclidean_common_target_right_productcoefficientscoefficientresiduebound. pfa_gap_euclidean_common_target_right_productcoefficientscoefficientresiduebound + S (pfc_value_euclidean_common_target_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_euclidean_common_target_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_euclidean_common_target_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_euclidean_common_target_right_productcoefficientscoefficient) + (p) * pfa_offset_left_euclidean_common_target_right_productcoefficientscoefficientresiduecongruence = (pfc_value_euclidean_common_target_right_productcoefficients) + (p) * pfa_offset_right_euclidean_common_target_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_euclidean_common_target_right_target pfrep_left_euclidean_common_target_right_target pfrep_right_euclidean_common_target_right_target. ((exists pfrep_position_euclidean_common_target_right_targetfirst. ((pfrep_position_euclidean_common_target_right_targetfirst+S (pfrep_power_euclidean_common_target_right_target)=(pfrd_plen_euclidean_common_target_right)) /\ ((((exists ff_h_pfp_euclidean_common_target_right_targetfirstentry. ff_h_pfp_euclidean_common_target_right_targetfirstentry + S (pfrep_left_euclidean_common_target_right_target) = S ((S (pfrep_position_euclidean_common_target_right_targetfirst)) * pfrd_pc_euclidean_common_target_right)) /\ exists ff_q_pfp_euclidean_common_target_right_targetfirstentry. pfrd_pb_euclidean_common_target_right = ff_q_pfp_euclidean_common_target_right_targetfirstentry * S ((S (pfrep_position_euclidean_common_target_right_targetfirst)) * pfrd_pc_euclidean_common_target_right) + (pfrep_left_euclidean_common_target_right_target)))))) \/ (((exists pfrep_gap_euclidean_common_target_right_targetfirstoutside. pfrep_gap_euclidean_common_target_right_targetfirstoutside+(pfrd_plen_euclidean_common_target_right)=(pfrep_power_euclidean_common_target_right_target)) /\ (((pfrep_left_euclidean_common_target_right_target)=0))))) -> ((exists pfrep_position_euclidean_common_target_right_targetsecond. ((pfrep_position_euclidean_common_target_right_targetsecond+S (pfrep_power_euclidean_common_target_right_target)=(N)) /\ ((((exists ff_h_pfp_euclidean_common_target_right_targetsecondentry. ff_h_pfp_euclidean_common_target_right_targetsecondentry + S (pfrep_right_euclidean_common_target_right_target) = S ((S (pfrep_position_euclidean_common_target_right_targetsecond)) * rc)) /\ exists ff_q_pfp_euclidean_common_target_right_targetsecondentry. rb = ff_q_pfp_euclidean_common_target_right_targetsecondentry * S ((S (pfrep_position_euclidean_common_target_right_targetsecond)) * rc) + (pfrep_right_euclidean_common_target_right_target)))))) \/ (((exists pfrep_gap_euclidean_common_target_right_targetsecondoutside. pfrep_gap_euclidean_common_target_right_targetsecondoutside+(N)=(pfrep_power_euclidean_common_target_right_target)) /\ (((pfrep_right_euclidean_common_target_right_target)=0))))) -> pfrep_left_euclidean_common_target_right_target=pfrep_right_euclidean_common_target_right_target))))))))))) /\ (((((((forall fom_index_pfp_euclidean_common_target_left_canonical. (exists fom_gap_pfp_euclidean_common_target_left_canonical_index_bound. fom_gap_pfp_euclidean_common_target_left_canonical_index_bound + S (fom_index_pfp_euclidean_common_target_left_canonical) = M) -> exists fom_value_pfp_euclidean_common_target_left_canonical. ((((exists fom_beta_height_pfp_euclidean_common_target_left_canonical_entry. fom_beta_height_pfp_euclidean_common_target_left_canonical_entry + S (fom_value_pfp_euclidean_common_target_left_canonical) = S ((S (fom_index_pfp_euclidean_common_target_left_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_left_canonical_entry. bb = fom_beta_quotient_pfp_euclidean_common_target_left_canonical_entry * S ((S (fom_index_pfp_euclidean_common_target_left_canonical)) * bc) + (fom_value_pfp_euclidean_common_target_left_canonical))) /\ (exists fom_gap_pfp_euclidean_common_target_left_canonical_value_bound. fom_gap_pfp_euclidean_common_target_left_canonical_value_bound + S (fom_value_pfp_euclidean_common_target_left_canonical) = p))) /\ ((exists pfrd_qb_euclidean_common_target_left pfrd_qc_euclidean_common_target_left pfrd_qlen_euclidean_common_target_left pfrd_pb_euclidean_common_target_left pfrd_pc_euclidean_common_target_left pfrd_plen_euclidean_common_target_left. ((((forall fom_index_pfp_euclidean_common_target_left_productleft. (exists fom_gap_pfp_euclidean_common_target_left_productleft_index_bound. fom_gap_pfp_euclidean_common_target_left_productleft_index_bound + S (fom_index_pfp_euclidean_common_target_left_productleft) = pfrd_qlen_euclidean_common_target_left) -> exists fom_value_pfp_euclidean_common_target_left_productleft. ((((exists fom_beta_height_pfp_euclidean_common_target_left_productleft_entry. fom_beta_height_pfp_euclidean_common_target_left_productleft_entry + S (fom_value_pfp_euclidean_common_target_left_productleft) = S ((S (fom_index_pfp_euclidean_common_target_left_productleft)) * pfrd_qc_euclidean_common_target_left)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_left_productleft_entry. pfrd_qb_euclidean_common_target_left = fom_beta_quotient_pfp_euclidean_common_target_left_productleft_entry * S ((S (fom_index_pfp_euclidean_common_target_left_productleft)) * pfrd_qc_euclidean_common_target_left) + (fom_value_pfp_euclidean_common_target_left_productleft))) /\ (exists fom_gap_pfp_euclidean_common_target_left_productleft_value_bound. fom_gap_pfp_euclidean_common_target_left_productleft_value_bound + S (fom_value_pfp_euclidean_common_target_left_productleft) = p))) /\ (((forall fom_index_pfp_euclidean_common_target_left_productright. (exists fom_gap_pfp_euclidean_common_target_left_productright_index_bound. fom_gap_pfp_euclidean_common_target_left_productright_index_bound + S (fom_index_pfp_euclidean_common_target_left_productright) = J) -> exists fom_value_pfp_euclidean_common_target_left_productright. ((((exists fom_beta_height_pfp_euclidean_common_target_left_productright_entry. fom_beta_height_pfp_euclidean_common_target_left_productright_entry + S (fom_value_pfp_euclidean_common_target_left_productright) = S ((S (fom_index_pfp_euclidean_common_target_left_productright)) * dc)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_left_productright_entry. db = fom_beta_quotient_pfp_euclidean_common_target_left_productright_entry * S ((S (fom_index_pfp_euclidean_common_target_left_productright)) * dc) + (fom_value_pfp_euclidean_common_target_left_productright))) /\ (exists fom_gap_pfp_euclidean_common_target_left_productright_value_bound. fom_gap_pfp_euclidean_common_target_left_productright_value_bound + S (fom_value_pfp_euclidean_common_target_left_productright) = p))) /\ (((((((pfrd_qlen_euclidean_common_target_left)=0 \/ (J)=0) /\ (((pfrd_plen_euclidean_common_target_left)=0)))) \/ (((~((pfrd_qlen_euclidean_common_target_left)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_euclidean_common_target_left)+(J)=S (pfrd_plen_euclidean_common_target_left)))))))) /\ ((forall pfc_index_euclidean_common_target_left_productcoefficients. (exists pfa_gap_euclidean_common_target_left_productcoefficientsbound. pfa_gap_euclidean_common_target_left_productcoefficientsbound + S (pfc_index_euclidean_common_target_left_productcoefficients) = (pfrd_plen_euclidean_common_target_left)) -> exists pfc_value_euclidean_common_target_left_productcoefficients. ((((exists ff_h_pfp_euclidean_common_target_left_productcoefficientsentry. ff_h_pfp_euclidean_common_target_left_productcoefficientsentry + S (pfc_value_euclidean_common_target_left_productcoefficients) = S ((S (pfc_index_euclidean_common_target_left_productcoefficients)) * pfrd_pc_euclidean_common_target_left)) /\ exists ff_q_pfp_euclidean_common_target_left_productcoefficientsentry. pfrd_pb_euclidean_common_target_left = ff_q_pfp_euclidean_common_target_left_productcoefficientsentry * S ((S (pfc_index_euclidean_common_target_left_productcoefficients)) * pfrd_pc_euclidean_common_target_left) + (pfc_value_euclidean_common_target_left_productcoefficients))) /\ ((exists pfc_terms_code_euclidean_common_target_left_productcoefficientscoefficient pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient pfc_natural_sum_euclidean_common_target_left_productcoefficientscoefficient. ((forall pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonalbound. pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_euclidean_common_target_left_productcoefficients))) -> exists pfc_value_euclidean_common_target_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_euclidean_common_target_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_euclidean_common_target_left_productcoefficientscoefficient = ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient) + (pfc_value_euclidean_common_target_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)+pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm=(pfc_index_euclidean_common_target_left_productcoefficients)) /\ ((((((exists pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal) = (pfrd_qlen_euclidean_common_target_left)) /\ ((((exists ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_target_left)) /\ exists ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_euclidean_common_target_left = ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_target_left) + (pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_euclidean_common_target_left)=(pfc_index_euclidean_common_target_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_euclidean_common_target_left_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_euclidean_common_target_left_productcoefficientscoefficientdiagonal)=pfc_left_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm*pfc_right_euclidean_common_target_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_euclidean_common_target_left_productcoefficientscoefficient) = S ((S (S (pfc_index_euclidean_common_target_left_productcoefficients))) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_euclidean_common_target_left_productcoefficients))) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum) + (pfc_natural_sum_euclidean_common_target_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_euclidean_common_target_left_productcoefficients)) -> exists fs_a_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_euclidean_common_target_left_productcoefficientscoefficient = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_target_left_productcoefficientscoefficient) + (fs_a_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum) + (fs_r_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_euclidean_common_target_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_left_productcoefficientscoefficientsum) + (fs_s_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_euclidean_common_target_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_euclidean_common_target_left_productcoefficientscoefficientresiduebound. pfa_gap_euclidean_common_target_left_productcoefficientscoefficientresiduebound + S (pfc_value_euclidean_common_target_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_euclidean_common_target_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_euclidean_common_target_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_euclidean_common_target_left_productcoefficientscoefficient) + (p) * pfa_offset_left_euclidean_common_target_left_productcoefficientscoefficientresiduecongruence = (pfc_value_euclidean_common_target_left_productcoefficients) + (p) * pfa_offset_right_euclidean_common_target_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_euclidean_common_target_left_target pfrep_left_euclidean_common_target_left_target pfrep_right_euclidean_common_target_left_target. ((exists pfrep_position_euclidean_common_target_left_targetfirst. ((pfrep_position_euclidean_common_target_left_targetfirst+S (pfrep_power_euclidean_common_target_left_target)=(pfrd_plen_euclidean_common_target_left)) /\ ((((exists ff_h_pfp_euclidean_common_target_left_targetfirstentry. ff_h_pfp_euclidean_common_target_left_targetfirstentry + S (pfrep_left_euclidean_common_target_left_target) = S ((S (pfrep_position_euclidean_common_target_left_targetfirst)) * pfrd_pc_euclidean_common_target_left)) /\ exists ff_q_pfp_euclidean_common_target_left_targetfirstentry. pfrd_pb_euclidean_common_target_left = ff_q_pfp_euclidean_common_target_left_targetfirstentry * S ((S (pfrep_position_euclidean_common_target_left_targetfirst)) * pfrd_pc_euclidean_common_target_left) + (pfrep_left_euclidean_common_target_left_target)))))) \/ (((exists pfrep_gap_euclidean_common_target_left_targetfirstoutside. pfrep_gap_euclidean_common_target_left_targetfirstoutside+(pfrd_plen_euclidean_common_target_left)=(pfrep_power_euclidean_common_target_left_target)) /\ (((pfrep_left_euclidean_common_target_left_target)=0))))) -> ((exists pfrep_position_euclidean_common_target_left_targetsecond. ((pfrep_position_euclidean_common_target_left_targetsecond+S (pfrep_power_euclidean_common_target_left_target)=(M)) /\ ((((exists ff_h_pfp_euclidean_common_target_left_targetsecondentry. ff_h_pfp_euclidean_common_target_left_targetsecondentry + S (pfrep_right_euclidean_common_target_left_target) = S ((S (pfrep_position_euclidean_common_target_left_targetsecond)) * bc)) /\ exists ff_q_pfp_euclidean_common_target_left_targetsecondentry. bb = ff_q_pfp_euclidean_common_target_left_targetsecondentry * S ((S (pfrep_position_euclidean_common_target_left_targetsecond)) * bc) + (pfrep_right_euclidean_common_target_left_target)))))) \/ (((exists pfrep_gap_euclidean_common_target_left_targetsecondoutside. pfrep_gap_euclidean_common_target_left_targetsecondoutside+(M)=(pfrep_power_euclidean_common_target_left_target)) /\ (((pfrep_right_euclidean_common_target_left_target)=0))))) -> pfrep_left_euclidean_common_target_left_target=pfrep_right_euclidean_common_target_left_target))))))) /\ ((((forall fom_index_pfp_euclidean_common_target_right_canonical. (exists fom_gap_pfp_euclidean_common_target_right_canonical_index_bound. fom_gap_pfp_euclidean_common_target_right_canonical_index_bound + S (fom_index_pfp_euclidean_common_target_right_canonical) = N) -> exists fom_value_pfp_euclidean_common_target_right_canonical. ((((exists fom_beta_height_pfp_euclidean_common_target_right_canonical_entry. fom_beta_height_pfp_euclidean_common_target_right_canonical_entry + S (fom_value_pfp_euclidean_common_target_right_canonical) = S ((S (fom_index_pfp_euclidean_common_target_right_canonical)) * rc)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_right_canonical_entry. rb = fom_beta_quotient_pfp_euclidean_common_target_right_canonical_entry * S ((S (fom_index_pfp_euclidean_common_target_right_canonical)) * rc) + (fom_value_pfp_euclidean_common_target_right_canonical))) /\ (exists fom_gap_pfp_euclidean_common_target_right_canonical_value_bound. fom_gap_pfp_euclidean_common_target_right_canonical_value_bound + S (fom_value_pfp_euclidean_common_target_right_canonical) = p))) /\ ((exists pfrd_qb_euclidean_common_target_right pfrd_qc_euclidean_common_target_right pfrd_qlen_euclidean_common_target_right pfrd_pb_euclidean_common_target_right pfrd_pc_euclidean_common_target_right pfrd_plen_euclidean_common_target_right. ((((forall fom_index_pfp_euclidean_common_target_right_productleft. (exists fom_gap_pfp_euclidean_common_target_right_productleft_index_bound. fom_gap_pfp_euclidean_common_target_right_productleft_index_bound + S (fom_index_pfp_euclidean_common_target_right_productleft) = pfrd_qlen_euclidean_common_target_right) -> exists fom_value_pfp_euclidean_common_target_right_productleft. ((((exists fom_beta_height_pfp_euclidean_common_target_right_productleft_entry. fom_beta_height_pfp_euclidean_common_target_right_productleft_entry + S (fom_value_pfp_euclidean_common_target_right_productleft) = S ((S (fom_index_pfp_euclidean_common_target_right_productleft)) * pfrd_qc_euclidean_common_target_right)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_right_productleft_entry. pfrd_qb_euclidean_common_target_right = fom_beta_quotient_pfp_euclidean_common_target_right_productleft_entry * S ((S (fom_index_pfp_euclidean_common_target_right_productleft)) * pfrd_qc_euclidean_common_target_right) + (fom_value_pfp_euclidean_common_target_right_productleft))) /\ (exists fom_gap_pfp_euclidean_common_target_right_productleft_value_bound. fom_gap_pfp_euclidean_common_target_right_productleft_value_bound + S (fom_value_pfp_euclidean_common_target_right_productleft) = p))) /\ (((forall fom_index_pfp_euclidean_common_target_right_productright. (exists fom_gap_pfp_euclidean_common_target_right_productright_index_bound. fom_gap_pfp_euclidean_common_target_right_productright_index_bound + S (fom_index_pfp_euclidean_common_target_right_productright) = J) -> exists fom_value_pfp_euclidean_common_target_right_productright. ((((exists fom_beta_height_pfp_euclidean_common_target_right_productright_entry. fom_beta_height_pfp_euclidean_common_target_right_productright_entry + S (fom_value_pfp_euclidean_common_target_right_productright) = S ((S (fom_index_pfp_euclidean_common_target_right_productright)) * dc)) /\ exists fom_beta_quotient_pfp_euclidean_common_target_right_productright_entry. db = fom_beta_quotient_pfp_euclidean_common_target_right_productright_entry * S ((S (fom_index_pfp_euclidean_common_target_right_productright)) * dc) + (fom_value_pfp_euclidean_common_target_right_productright))) /\ (exists fom_gap_pfp_euclidean_common_target_right_productright_value_bound. fom_gap_pfp_euclidean_common_target_right_productright_value_bound + S (fom_value_pfp_euclidean_common_target_right_productright) = p))) /\ (((((((pfrd_qlen_euclidean_common_target_right)=0 \/ (J)=0) /\ (((pfrd_plen_euclidean_common_target_right)=0)))) \/ (((~((pfrd_qlen_euclidean_common_target_right)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_euclidean_common_target_right)+(J)=S (pfrd_plen_euclidean_common_target_right)))))))) /\ ((forall pfc_index_euclidean_common_target_right_productcoefficients. (exists pfa_gap_euclidean_common_target_right_productcoefficientsbound. pfa_gap_euclidean_common_target_right_productcoefficientsbound + S (pfc_index_euclidean_common_target_right_productcoefficients) = (pfrd_plen_euclidean_common_target_right)) -> exists pfc_value_euclidean_common_target_right_productcoefficients. ((((exists ff_h_pfp_euclidean_common_target_right_productcoefficientsentry. ff_h_pfp_euclidean_common_target_right_productcoefficientsentry + S (pfc_value_euclidean_common_target_right_productcoefficients) = S ((S (pfc_index_euclidean_common_target_right_productcoefficients)) * pfrd_pc_euclidean_common_target_right)) /\ exists ff_q_pfp_euclidean_common_target_right_productcoefficientsentry. pfrd_pb_euclidean_common_target_right = ff_q_pfp_euclidean_common_target_right_productcoefficientsentry * S ((S (pfc_index_euclidean_common_target_right_productcoefficients)) * pfrd_pc_euclidean_common_target_right) + (pfc_value_euclidean_common_target_right_productcoefficients))) /\ ((exists pfc_terms_code_euclidean_common_target_right_productcoefficientscoefficient pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient pfc_natural_sum_euclidean_common_target_right_productcoefficientscoefficient. ((forall pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonalbound. pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_euclidean_common_target_right_productcoefficients))) -> exists pfc_value_euclidean_common_target_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_euclidean_common_target_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_euclidean_common_target_right_productcoefficientscoefficient = ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient) + (pfc_value_euclidean_common_target_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)+pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm=(pfc_index_euclidean_common_target_right_productcoefficients)) /\ ((((((exists pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal) = (pfrd_qlen_euclidean_common_target_right)) /\ ((((exists ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_target_right)) /\ exists ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_euclidean_common_target_right = ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_target_right) + (pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_euclidean_common_target_right)=(pfc_index_euclidean_common_target_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_euclidean_common_target_right_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_euclidean_common_target_right_productcoefficientscoefficientdiagonal)=pfc_left_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm*pfc_right_euclidean_common_target_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_euclidean_common_target_right_productcoefficientscoefficient) = S ((S (S (pfc_index_euclidean_common_target_right_productcoefficients))) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_euclidean_common_target_right_productcoefficients))) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum) + (pfc_natural_sum_euclidean_common_target_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_euclidean_common_target_right_productcoefficients)) -> exists fs_a_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_euclidean_common_target_right_productcoefficientscoefficient = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_target_right_productcoefficientscoefficient) + (fs_a_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum) + (fs_r_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_euclidean_common_target_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_target_right_productcoefficientscoefficientsum) + (fs_s_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_euclidean_common_target_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_euclidean_common_target_right_productcoefficientscoefficientresiduebound. pfa_gap_euclidean_common_target_right_productcoefficientscoefficientresiduebound + S (pfc_value_euclidean_common_target_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_euclidean_common_target_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_euclidean_common_target_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_euclidean_common_target_right_productcoefficientscoefficient) + (p) * pfa_offset_left_euclidean_common_target_right_productcoefficientscoefficientresiduecongruence = (pfc_value_euclidean_common_target_right_productcoefficients) + (p) * pfa_offset_right_euclidean_common_target_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_euclidean_common_target_right_target pfrep_left_euclidean_common_target_right_target pfrep_right_euclidean_common_target_right_target. ((exists pfrep_position_euclidean_common_target_right_targetfirst. ((pfrep_position_euclidean_common_target_right_targetfirst+S (pfrep_power_euclidean_common_target_right_target)=(pfrd_plen_euclidean_common_target_right)) /\ ((((exists ff_h_pfp_euclidean_common_target_right_targetfirstentry. ff_h_pfp_euclidean_common_target_right_targetfirstentry + S (pfrep_left_euclidean_common_target_right_target) = S ((S (pfrep_position_euclidean_common_target_right_targetfirst)) * pfrd_pc_euclidean_common_target_right)) /\ exists ff_q_pfp_euclidean_common_target_right_targetfirstentry. pfrd_pb_euclidean_common_target_right = ff_q_pfp_euclidean_common_target_right_targetfirstentry * S ((S (pfrep_position_euclidean_common_target_right_targetfirst)) * pfrd_pc_euclidean_common_target_right) + (pfrep_left_euclidean_common_target_right_target)))))) \/ (((exists pfrep_gap_euclidean_common_target_right_targetfirstoutside. pfrep_gap_euclidean_common_target_right_targetfirstoutside+(pfrd_plen_euclidean_common_target_right)=(pfrep_power_euclidean_common_target_right_target)) /\ (((pfrep_left_euclidean_common_target_right_target)=0))))) -> ((exists pfrep_position_euclidean_common_target_right_targetsecond. ((pfrep_position_euclidean_common_target_right_targetsecond+S (pfrep_power_euclidean_common_target_right_target)=(N)) /\ ((((exists ff_h_pfp_euclidean_common_target_right_targetsecondentry. ff_h_pfp_euclidean_common_target_right_targetsecondentry + S (pfrep_right_euclidean_common_target_right_target) = S ((S (pfrep_position_euclidean_common_target_right_targetsecond)) * rc)) /\ exists ff_q_pfp_euclidean_common_target_right_targetsecondentry. rb = ff_q_pfp_euclidean_common_target_right_targetsecondentry * S ((S (pfrep_position_euclidean_common_target_right_targetsecond)) * rc) + (pfrep_right_euclidean_common_target_right_target)))))) \/ (((exists pfrep_gap_euclidean_common_target_right_targetsecondoutside. pfrep_gap_euclidean_common_target_right_targetsecondoutside+(N)=(pfrep_power_euclidean_common_target_right_target)) /\ (((pfrep_right_euclidean_common_target_right_target)=0))))) -> pfrep_left_euclidean_common_target_right_target=pfrep_right_euclidean_common_target_right_target)))))))))) -> (((((forall fom_index_pfp_euclidean_common_source_left_canonical. (exists fom_gap_pfp_euclidean_common_source_left_canonical_index_bound. fom_gap_pfp_euclidean_common_source_left_canonical_index_bound + S (fom_index_pfp_euclidean_common_source_left_canonical) = L) -> exists fom_value_pfp_euclidean_common_source_left_canonical. ((((exists fom_beta_height_pfp_euclidean_common_source_left_canonical_entry. fom_beta_height_pfp_euclidean_common_source_left_canonical_entry + S (fom_value_pfp_euclidean_common_source_left_canonical) = S ((S (fom_index_pfp_euclidean_common_source_left_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_left_canonical_entry. ab = fom_beta_quotient_pfp_euclidean_common_source_left_canonical_entry * S ((S (fom_index_pfp_euclidean_common_source_left_canonical)) * ac) + (fom_value_pfp_euclidean_common_source_left_canonical))) /\ (exists fom_gap_pfp_euclidean_common_source_left_canonical_value_bound. fom_gap_pfp_euclidean_common_source_left_canonical_value_bound + S (fom_value_pfp_euclidean_common_source_left_canonical) = p))) /\ ((exists pfrd_qb_euclidean_common_source_left pfrd_qc_euclidean_common_source_left pfrd_qlen_euclidean_common_source_left pfrd_pb_euclidean_common_source_left pfrd_pc_euclidean_common_source_left pfrd_plen_euclidean_common_source_left. ((((forall fom_index_pfp_euclidean_common_source_left_productleft. (exists fom_gap_pfp_euclidean_common_source_left_productleft_index_bound. fom_gap_pfp_euclidean_common_source_left_productleft_index_bound + S (fom_index_pfp_euclidean_common_source_left_productleft) = pfrd_qlen_euclidean_common_source_left) -> exists fom_value_pfp_euclidean_common_source_left_productleft. ((((exists fom_beta_height_pfp_euclidean_common_source_left_productleft_entry. fom_beta_height_pfp_euclidean_common_source_left_productleft_entry + S (fom_value_pfp_euclidean_common_source_left_productleft) = S ((S (fom_index_pfp_euclidean_common_source_left_productleft)) * pfrd_qc_euclidean_common_source_left)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_left_productleft_entry. pfrd_qb_euclidean_common_source_left = fom_beta_quotient_pfp_euclidean_common_source_left_productleft_entry * S ((S (fom_index_pfp_euclidean_common_source_left_productleft)) * pfrd_qc_euclidean_common_source_left) + (fom_value_pfp_euclidean_common_source_left_productleft))) /\ (exists fom_gap_pfp_euclidean_common_source_left_productleft_value_bound. fom_gap_pfp_euclidean_common_source_left_productleft_value_bound + S (fom_value_pfp_euclidean_common_source_left_productleft) = p))) /\ (((forall fom_index_pfp_euclidean_common_source_left_productright. (exists fom_gap_pfp_euclidean_common_source_left_productright_index_bound. fom_gap_pfp_euclidean_common_source_left_productright_index_bound + S (fom_index_pfp_euclidean_common_source_left_productright) = J) -> exists fom_value_pfp_euclidean_common_source_left_productright. ((((exists fom_beta_height_pfp_euclidean_common_source_left_productright_entry. fom_beta_height_pfp_euclidean_common_source_left_productright_entry + S (fom_value_pfp_euclidean_common_source_left_productright) = S ((S (fom_index_pfp_euclidean_common_source_left_productright)) * dc)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_left_productright_entry. db = fom_beta_quotient_pfp_euclidean_common_source_left_productright_entry * S ((S (fom_index_pfp_euclidean_common_source_left_productright)) * dc) + (fom_value_pfp_euclidean_common_source_left_productright))) /\ (exists fom_gap_pfp_euclidean_common_source_left_productright_value_bound. fom_gap_pfp_euclidean_common_source_left_productright_value_bound + S (fom_value_pfp_euclidean_common_source_left_productright) = p))) /\ (((((((pfrd_qlen_euclidean_common_source_left)=0 \/ (J)=0) /\ (((pfrd_plen_euclidean_common_source_left)=0)))) \/ (((~((pfrd_qlen_euclidean_common_source_left)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_euclidean_common_source_left)+(J)=S (pfrd_plen_euclidean_common_source_left)))))))) /\ ((forall pfc_index_euclidean_common_source_left_productcoefficients. (exists pfa_gap_euclidean_common_source_left_productcoefficientsbound. pfa_gap_euclidean_common_source_left_productcoefficientsbound + S (pfc_index_euclidean_common_source_left_productcoefficients) = (pfrd_plen_euclidean_common_source_left)) -> exists pfc_value_euclidean_common_source_left_productcoefficients. ((((exists ff_h_pfp_euclidean_common_source_left_productcoefficientsentry. ff_h_pfp_euclidean_common_source_left_productcoefficientsentry + S (pfc_value_euclidean_common_source_left_productcoefficients) = S ((S (pfc_index_euclidean_common_source_left_productcoefficients)) * pfrd_pc_euclidean_common_source_left)) /\ exists ff_q_pfp_euclidean_common_source_left_productcoefficientsentry. pfrd_pb_euclidean_common_source_left = ff_q_pfp_euclidean_common_source_left_productcoefficientsentry * S ((S (pfc_index_euclidean_common_source_left_productcoefficients)) * pfrd_pc_euclidean_common_source_left) + (pfc_value_euclidean_common_source_left_productcoefficients))) /\ ((exists pfc_terms_code_euclidean_common_source_left_productcoefficientscoefficient pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient pfc_natural_sum_euclidean_common_source_left_productcoefficientscoefficient. ((forall pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonalbound. pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_euclidean_common_source_left_productcoefficients))) -> exists pfc_value_euclidean_common_source_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_euclidean_common_source_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_euclidean_common_source_left_productcoefficientscoefficient = ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient) + (pfc_value_euclidean_common_source_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)+pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm=(pfc_index_euclidean_common_source_left_productcoefficients)) /\ ((((((exists pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal) = (pfrd_qlen_euclidean_common_source_left)) /\ ((((exists ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_source_left)) /\ exists ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_euclidean_common_source_left = ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_source_left) + (pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_euclidean_common_source_left)=(pfc_index_euclidean_common_source_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_euclidean_common_source_left_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_euclidean_common_source_left_productcoefficientscoefficientdiagonal)=pfc_left_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm*pfc_right_euclidean_common_source_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_euclidean_common_source_left_productcoefficientscoefficient) = S ((S (S (pfc_index_euclidean_common_source_left_productcoefficients))) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_euclidean_common_source_left_productcoefficients))) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum) + (pfc_natural_sum_euclidean_common_source_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_euclidean_common_source_left_productcoefficients)) -> exists fs_a_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_euclidean_common_source_left_productcoefficientscoefficient = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_source_left_productcoefficientscoefficient) + (fs_a_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum) + (fs_r_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_euclidean_common_source_left_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_left_productcoefficientscoefficientsum) + (fs_s_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_euclidean_common_source_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_euclidean_common_source_left_productcoefficientscoefficientresiduebound. pfa_gap_euclidean_common_source_left_productcoefficientscoefficientresiduebound + S (pfc_value_euclidean_common_source_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_euclidean_common_source_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_euclidean_common_source_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_euclidean_common_source_left_productcoefficientscoefficient) + (p) * pfa_offset_left_euclidean_common_source_left_productcoefficientscoefficientresiduecongruence = (pfc_value_euclidean_common_source_left_productcoefficients) + (p) * pfa_offset_right_euclidean_common_source_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_euclidean_common_source_left_target pfrep_left_euclidean_common_source_left_target pfrep_right_euclidean_common_source_left_target. ((exists pfrep_position_euclidean_common_source_left_targetfirst. ((pfrep_position_euclidean_common_source_left_targetfirst+S (pfrep_power_euclidean_common_source_left_target)=(pfrd_plen_euclidean_common_source_left)) /\ ((((exists ff_h_pfp_euclidean_common_source_left_targetfirstentry. ff_h_pfp_euclidean_common_source_left_targetfirstentry + S (pfrep_left_euclidean_common_source_left_target) = S ((S (pfrep_position_euclidean_common_source_left_targetfirst)) * pfrd_pc_euclidean_common_source_left)) /\ exists ff_q_pfp_euclidean_common_source_left_targetfirstentry. pfrd_pb_euclidean_common_source_left = ff_q_pfp_euclidean_common_source_left_targetfirstentry * S ((S (pfrep_position_euclidean_common_source_left_targetfirst)) * pfrd_pc_euclidean_common_source_left) + (pfrep_left_euclidean_common_source_left_target)))))) \/ (((exists pfrep_gap_euclidean_common_source_left_targetfirstoutside. pfrep_gap_euclidean_common_source_left_targetfirstoutside+(pfrd_plen_euclidean_common_source_left)=(pfrep_power_euclidean_common_source_left_target)) /\ (((pfrep_left_euclidean_common_source_left_target)=0))))) -> ((exists pfrep_position_euclidean_common_source_left_targetsecond. ((pfrep_position_euclidean_common_source_left_targetsecond+S (pfrep_power_euclidean_common_source_left_target)=(L)) /\ ((((exists ff_h_pfp_euclidean_common_source_left_targetsecondentry. ff_h_pfp_euclidean_common_source_left_targetsecondentry + S (pfrep_right_euclidean_common_source_left_target) = S ((S (pfrep_position_euclidean_common_source_left_targetsecond)) * ac)) /\ exists ff_q_pfp_euclidean_common_source_left_targetsecondentry. ab = ff_q_pfp_euclidean_common_source_left_targetsecondentry * S ((S (pfrep_position_euclidean_common_source_left_targetsecond)) * ac) + (pfrep_right_euclidean_common_source_left_target)))))) \/ (((exists pfrep_gap_euclidean_common_source_left_targetsecondoutside. pfrep_gap_euclidean_common_source_left_targetsecondoutside+(L)=(pfrep_power_euclidean_common_source_left_target)) /\ (((pfrep_right_euclidean_common_source_left_target)=0))))) -> pfrep_left_euclidean_common_source_left_target=pfrep_right_euclidean_common_source_left_target))))))) /\ ((((forall fom_index_pfp_euclidean_common_source_right_canonical. (exists fom_gap_pfp_euclidean_common_source_right_canonical_index_bound. fom_gap_pfp_euclidean_common_source_right_canonical_index_bound + S (fom_index_pfp_euclidean_common_source_right_canonical) = M) -> exists fom_value_pfp_euclidean_common_source_right_canonical. ((((exists fom_beta_height_pfp_euclidean_common_source_right_canonical_entry. fom_beta_height_pfp_euclidean_common_source_right_canonical_entry + S (fom_value_pfp_euclidean_common_source_right_canonical) = S ((S (fom_index_pfp_euclidean_common_source_right_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_right_canonical_entry. bb = fom_beta_quotient_pfp_euclidean_common_source_right_canonical_entry * S ((S (fom_index_pfp_euclidean_common_source_right_canonical)) * bc) + (fom_value_pfp_euclidean_common_source_right_canonical))) /\ (exists fom_gap_pfp_euclidean_common_source_right_canonical_value_bound. fom_gap_pfp_euclidean_common_source_right_canonical_value_bound + S (fom_value_pfp_euclidean_common_source_right_canonical) = p))) /\ ((exists pfrd_qb_euclidean_common_source_right pfrd_qc_euclidean_common_source_right pfrd_qlen_euclidean_common_source_right pfrd_pb_euclidean_common_source_right pfrd_pc_euclidean_common_source_right pfrd_plen_euclidean_common_source_right. ((((forall fom_index_pfp_euclidean_common_source_right_productleft. (exists fom_gap_pfp_euclidean_common_source_right_productleft_index_bound. fom_gap_pfp_euclidean_common_source_right_productleft_index_bound + S (fom_index_pfp_euclidean_common_source_right_productleft) = pfrd_qlen_euclidean_common_source_right) -> exists fom_value_pfp_euclidean_common_source_right_productleft. ((((exists fom_beta_height_pfp_euclidean_common_source_right_productleft_entry. fom_beta_height_pfp_euclidean_common_source_right_productleft_entry + S (fom_value_pfp_euclidean_common_source_right_productleft) = S ((S (fom_index_pfp_euclidean_common_source_right_productleft)) * pfrd_qc_euclidean_common_source_right)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_right_productleft_entry. pfrd_qb_euclidean_common_source_right = fom_beta_quotient_pfp_euclidean_common_source_right_productleft_entry * S ((S (fom_index_pfp_euclidean_common_source_right_productleft)) * pfrd_qc_euclidean_common_source_right) + (fom_value_pfp_euclidean_common_source_right_productleft))) /\ (exists fom_gap_pfp_euclidean_common_source_right_productleft_value_bound. fom_gap_pfp_euclidean_common_source_right_productleft_value_bound + S (fom_value_pfp_euclidean_common_source_right_productleft) = p))) /\ (((forall fom_index_pfp_euclidean_common_source_right_productright. (exists fom_gap_pfp_euclidean_common_source_right_productright_index_bound. fom_gap_pfp_euclidean_common_source_right_productright_index_bound + S (fom_index_pfp_euclidean_common_source_right_productright) = J) -> exists fom_value_pfp_euclidean_common_source_right_productright. ((((exists fom_beta_height_pfp_euclidean_common_source_right_productright_entry. fom_beta_height_pfp_euclidean_common_source_right_productright_entry + S (fom_value_pfp_euclidean_common_source_right_productright) = S ((S (fom_index_pfp_euclidean_common_source_right_productright)) * dc)) /\ exists fom_beta_quotient_pfp_euclidean_common_source_right_productright_entry. db = fom_beta_quotient_pfp_euclidean_common_source_right_productright_entry * S ((S (fom_index_pfp_euclidean_common_source_right_productright)) * dc) + (fom_value_pfp_euclidean_common_source_right_productright))) /\ (exists fom_gap_pfp_euclidean_common_source_right_productright_value_bound. fom_gap_pfp_euclidean_common_source_right_productright_value_bound + S (fom_value_pfp_euclidean_common_source_right_productright) = p))) /\ (((((((pfrd_qlen_euclidean_common_source_right)=0 \/ (J)=0) /\ (((pfrd_plen_euclidean_common_source_right)=0)))) \/ (((~((pfrd_qlen_euclidean_common_source_right)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_euclidean_common_source_right)+(J)=S (pfrd_plen_euclidean_common_source_right)))))))) /\ ((forall pfc_index_euclidean_common_source_right_productcoefficients. (exists pfa_gap_euclidean_common_source_right_productcoefficientsbound. pfa_gap_euclidean_common_source_right_productcoefficientsbound + S (pfc_index_euclidean_common_source_right_productcoefficients) = (pfrd_plen_euclidean_common_source_right)) -> exists pfc_value_euclidean_common_source_right_productcoefficients. ((((exists ff_h_pfp_euclidean_common_source_right_productcoefficientsentry. ff_h_pfp_euclidean_common_source_right_productcoefficientsentry + S (pfc_value_euclidean_common_source_right_productcoefficients) = S ((S (pfc_index_euclidean_common_source_right_productcoefficients)) * pfrd_pc_euclidean_common_source_right)) /\ exists ff_q_pfp_euclidean_common_source_right_productcoefficientsentry. pfrd_pb_euclidean_common_source_right = ff_q_pfp_euclidean_common_source_right_productcoefficientsentry * S ((S (pfc_index_euclidean_common_source_right_productcoefficients)) * pfrd_pc_euclidean_common_source_right) + (pfc_value_euclidean_common_source_right_productcoefficients))) /\ ((exists pfc_terms_code_euclidean_common_source_right_productcoefficientscoefficient pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient pfc_natural_sum_euclidean_common_source_right_productcoefficientscoefficient. ((forall pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonalbound. pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_euclidean_common_source_right_productcoefficients))) -> exists pfc_value_euclidean_common_source_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_euclidean_common_source_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_euclidean_common_source_right_productcoefficientscoefficient = ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient) + (pfc_value_euclidean_common_source_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)+pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm=(pfc_index_euclidean_common_source_right_productcoefficients)) /\ ((((((exists pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal) = (pfrd_qlen_euclidean_common_source_right)) /\ ((((exists ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_source_right)) /\ exists ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_euclidean_common_source_right = ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) * pfrd_qc_euclidean_common_source_right) + (pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_euclidean_common_source_right)=(pfc_index_euclidean_common_source_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_euclidean_common_source_right_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_euclidean_common_source_right_productcoefficientscoefficientdiagonal)=pfc_left_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm*pfc_right_euclidean_common_source_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_euclidean_common_source_right_productcoefficientscoefficient) = S ((S (S (pfc_index_euclidean_common_source_right_productcoefficients))) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_euclidean_common_source_right_productcoefficients))) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum) + (pfc_natural_sum_euclidean_common_source_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_euclidean_common_source_right_productcoefficients)) -> exists fs_a_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_euclidean_common_source_right_productcoefficientscoefficient = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_euclidean_common_source_right_productcoefficientscoefficient) + (fs_a_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum) + (fs_r_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_euclidean_common_source_right_productcoefficientscoefficientsum = fs_q_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_euclidean_common_source_right_productcoefficientscoefficientsum) + (fs_s_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_euclidean_common_source_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_euclidean_common_source_right_productcoefficientscoefficientresiduebound. pfa_gap_euclidean_common_source_right_productcoefficientscoefficientresiduebound + S (pfc_value_euclidean_common_source_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_euclidean_common_source_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_euclidean_common_source_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_euclidean_common_source_right_productcoefficientscoefficient) + (p) * pfa_offset_left_euclidean_common_source_right_productcoefficientscoefficientresiduecongruence = (pfc_value_euclidean_common_source_right_productcoefficients) + (p) * pfa_offset_right_euclidean_common_source_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_euclidean_common_source_right_target pfrep_left_euclidean_common_source_right_target pfrep_right_euclidean_common_source_right_target. ((exists pfrep_position_euclidean_common_source_right_targetfirst. ((pfrep_position_euclidean_common_source_right_targetfirst+S (pfrep_power_euclidean_common_source_right_target)=(pfrd_plen_euclidean_common_source_right)) /\ ((((exists ff_h_pfp_euclidean_common_source_right_targetfirstentry. ff_h_pfp_euclidean_common_source_right_targetfirstentry + S (pfrep_left_euclidean_common_source_right_target) = S ((S (pfrep_position_euclidean_common_source_right_targetfirst)) * pfrd_pc_euclidean_common_source_right)) /\ exists ff_q_pfp_euclidean_common_source_right_targetfirstentry. pfrd_pb_euclidean_common_source_right = ff_q_pfp_euclidean_common_source_right_targetfirstentry * S ((S (pfrep_position_euclidean_common_source_right_targetfirst)) * pfrd_pc_euclidean_common_source_right) + (pfrep_left_euclidean_common_source_right_target)))))) \/ (((exists pfrep_gap_euclidean_common_source_right_targetfirstoutside. pfrep_gap_euclidean_common_source_right_targetfirstoutside+(pfrd_plen_euclidean_common_source_right)=(pfrep_power_euclidean_common_source_right_target)) /\ (((pfrep_left_euclidean_common_source_right_target)=0))))) -> ((exists pfrep_position_euclidean_common_source_right_targetsecond. ((pfrep_position_euclidean_common_source_right_targetsecond+S (pfrep_power_euclidean_common_source_right_target)=(M)) /\ ((((exists ff_h_pfp_euclidean_common_source_right_targetsecondentry. ff_h_pfp_euclidean_common_source_right_targetsecondentry + S (pfrep_right_euclidean_common_source_right_target) = S ((S (pfrep_position_euclidean_common_source_right_targetsecond)) * bc)) /\ exists ff_q_pfp_euclidean_common_source_right_targetsecondentry. bb = ff_q_pfp_euclidean_common_source_right_targetsecondentry * S ((S (pfrep_position_euclidean_common_source_right_targetsecond)) * bc) + (pfrep_right_euclidean_common_source_right_target)))))) \/ (((exists pfrep_gap_euclidean_common_source_right_targetsecondoutside. pfrep_gap_euclidean_common_source_right_targetsecondoutside+(M)=(pfrep_power_euclidean_common_source_right_target)) /\ (((pfrep_right_euclidean_common_source_right_target)=0))))) -> pfrep_left_euclidean_common_source_right_target=pfrep_right_euclidean_common_source_right_target))))))))))))))