prime_field_polynomial_right_divides_transitive

Exact expanded first-order arithmetic statement

forall p db dc D ab ac L bb bc M. (~((p) = 1) /\ forall pfa_factor_left_right_transitive_prime pfa_factor_right_right_transitive_prime. (p) = pfa_factor_left_right_transitive_prime * pfa_factor_right_right_transitive_prime -> pfa_factor_left_right_transitive_prime = 1 \/ pfa_factor_right_right_transitive_prime = 1) -> (((forall fom_index_pfp_right_transitive_first_canonical. (exists fom_gap_pfp_right_transitive_first_canonical_index_bound. fom_gap_pfp_right_transitive_first_canonical_index_bound + S (fom_index_pfp_right_transitive_first_canonical) = L) -> exists fom_value_pfp_right_transitive_first_canonical. ((((exists fom_beta_height_pfp_right_transitive_first_canonical_entry. fom_beta_height_pfp_right_transitive_first_canonical_entry + S (fom_value_pfp_right_transitive_first_canonical) = S ((S (fom_index_pfp_right_transitive_first_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_right_transitive_first_canonical_entry. ab = fom_beta_quotient_pfp_right_transitive_first_canonical_entry * S ((S (fom_index_pfp_right_transitive_first_canonical)) * ac) + (fom_value_pfp_right_transitive_first_canonical))) /\ (exists fom_gap_pfp_right_transitive_first_canonical_value_bound. fom_gap_pfp_right_transitive_first_canonical_value_bound + S (fom_value_pfp_right_transitive_first_canonical) = p))) /\ ((exists pfrd_qb_right_transitive_first pfrd_qc_right_transitive_first pfrd_qlen_right_transitive_first pfrd_pb_right_transitive_first pfrd_pc_right_transitive_first pfrd_plen_right_transitive_first. ((((forall fom_index_pfp_right_transitive_first_productleft. (exists fom_gap_pfp_right_transitive_first_productleft_index_bound. fom_gap_pfp_right_transitive_first_productleft_index_bound + S (fom_index_pfp_right_transitive_first_productleft) = pfrd_qlen_right_transitive_first) -> exists fom_value_pfp_right_transitive_first_productleft. ((((exists fom_beta_height_pfp_right_transitive_first_productleft_entry. fom_beta_height_pfp_right_transitive_first_productleft_entry + S (fom_value_pfp_right_transitive_first_productleft) = S ((S (fom_index_pfp_right_transitive_first_productleft)) * pfrd_qc_right_transitive_first)) /\ exists fom_beta_quotient_pfp_right_transitive_first_productleft_entry. pfrd_qb_right_transitive_first = fom_beta_quotient_pfp_right_transitive_first_productleft_entry * S ((S (fom_index_pfp_right_transitive_first_productleft)) * pfrd_qc_right_transitive_first) + (fom_value_pfp_right_transitive_first_productleft))) /\ (exists fom_gap_pfp_right_transitive_first_productleft_value_bound. fom_gap_pfp_right_transitive_first_productleft_value_bound + S (fom_value_pfp_right_transitive_first_productleft) = p))) /\ (((forall fom_index_pfp_right_transitive_first_productright. (exists fom_gap_pfp_right_transitive_first_productright_index_bound. fom_gap_pfp_right_transitive_first_productright_index_bound + S (fom_index_pfp_right_transitive_first_productright) = D) -> exists fom_value_pfp_right_transitive_first_productright. ((((exists fom_beta_height_pfp_right_transitive_first_productright_entry. fom_beta_height_pfp_right_transitive_first_productright_entry + S (fom_value_pfp_right_transitive_first_productright) = S ((S (fom_index_pfp_right_transitive_first_productright)) * dc)) /\ exists fom_beta_quotient_pfp_right_transitive_first_productright_entry. db = fom_beta_quotient_pfp_right_transitive_first_productright_entry * S ((S (fom_index_pfp_right_transitive_first_productright)) * dc) + (fom_value_pfp_right_transitive_first_productright))) /\ (exists fom_gap_pfp_right_transitive_first_productright_value_bound. fom_gap_pfp_right_transitive_first_productright_value_bound + S (fom_value_pfp_right_transitive_first_productright) = p))) /\ (((((((pfrd_qlen_right_transitive_first)=0 \/ (D)=0) /\ (((pfrd_plen_right_transitive_first)=0)))) \/ (((~((pfrd_qlen_right_transitive_first)=0)) /\ (((~((D)=0)) /\ (((pfrd_qlen_right_transitive_first)+(D)=S (pfrd_plen_right_transitive_first)))))))) /\ ((forall pfc_index_right_transitive_first_productcoefficients. (exists pfa_gap_right_transitive_first_productcoefficientsbound. pfa_gap_right_transitive_first_productcoefficientsbound + S (pfc_index_right_transitive_first_productcoefficients) = (pfrd_plen_right_transitive_first)) -> exists pfc_value_right_transitive_first_productcoefficients. ((((exists ff_h_pfp_right_transitive_first_productcoefficientsentry. ff_h_pfp_right_transitive_first_productcoefficientsentry + S (pfc_value_right_transitive_first_productcoefficients) = S ((S (pfc_index_right_transitive_first_productcoefficients)) * pfrd_pc_right_transitive_first)) /\ exists ff_q_pfp_right_transitive_first_productcoefficientsentry. pfrd_pb_right_transitive_first = ff_q_pfp_right_transitive_first_productcoefficientsentry * S ((S (pfc_index_right_transitive_first_productcoefficients)) * pfrd_pc_right_transitive_first) + (pfc_value_right_transitive_first_productcoefficients))) /\ ((exists pfc_terms_code_right_transitive_first_productcoefficientscoefficient pfc_terms_scale_right_transitive_first_productcoefficientscoefficient pfc_natural_sum_right_transitive_first_productcoefficientscoefficient. ((forall pfc_index_right_transitive_first_productcoefficientscoefficientdiagonal. (exists pfa_gap_right_transitive_first_productcoefficientscoefficientdiagonalbound. pfa_gap_right_transitive_first_productcoefficientscoefficientdiagonalbound + S (pfc_index_right_transitive_first_productcoefficientscoefficientdiagonal) = (S (pfc_index_right_transitive_first_productcoefficients))) -> exists pfc_value_right_transitive_first_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_right_transitive_first_productcoefficientscoefficientdiagonalentry. ff_h_pfp_right_transitive_first_productcoefficientscoefficientdiagonalentry + S (pfc_value_right_transitive_first_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_right_transitive_first_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_transitive_first_productcoefficientscoefficient)) /\ exists ff_q_pfp_right_transitive_first_productcoefficientscoefficientdiagonalentry. pfc_terms_code_right_transitive_first_productcoefficientscoefficient = ff_q_pfp_right_transitive_first_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_right_transitive_first_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_transitive_first_productcoefficientscoefficient) + (pfc_value_right_transitive_first_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_right_transitive_first_productcoefficientscoefficientdiagonalterm pfc_left_right_transitive_first_productcoefficientscoefficientdiagonalterm pfc_right_right_transitive_first_productcoefficientscoefficientdiagonalterm. (((pfc_index_right_transitive_first_productcoefficientscoefficientdiagonal)+pfc_complement_right_transitive_first_productcoefficientscoefficientdiagonalterm=(pfc_index_right_transitive_first_productcoefficients)) /\ ((((((exists pfa_gap_right_transitive_first_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_right_transitive_first_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_right_transitive_first_productcoefficientscoefficientdiagonal) = (pfrd_qlen_right_transitive_first)) /\ ((((exists ff_h_pfp_right_transitive_first_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_right_transitive_first_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_right_transitive_first_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_right_transitive_first_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_transitive_first)) /\ exists ff_q_pfp_right_transitive_first_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_right_transitive_first = ff_q_pfp_right_transitive_first_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_right_transitive_first_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_transitive_first) + (pfc_left_right_transitive_first_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_transitive_first_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_right_transitive_first_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_right_transitive_first)=(pfc_index_right_transitive_first_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_right_transitive_first_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_right_transitive_first_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_right_transitive_first_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_right_transitive_first_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_right_transitive_first_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_right_transitive_first_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_right_transitive_first_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_right_transitive_first_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_right_transitive_first_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_right_transitive_first_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_right_transitive_first_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_right_transitive_first_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_transitive_first_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_right_transitive_first_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_right_transitive_first_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_right_transitive_first_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_right_transitive_first_productcoefficientscoefficientdiagonal)=pfc_left_right_transitive_first_productcoefficientscoefficientdiagonalterm*pfc_right_right_transitive_first_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_right_transitive_first_productcoefficientscoefficientsum fs_v_pfc_right_transitive_first_productcoefficientscoefficientsum. ((((exists fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_start. fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_right_transitive_first_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_start. fs_u_pfc_right_transitive_first_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_right_transitive_first_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_right_transitive_first_productcoefficientscoefficient) = S ((S (S (pfc_index_right_transitive_first_productcoefficients))) * fs_v_pfc_right_transitive_first_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_right_transitive_first_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_right_transitive_first_productcoefficients))) * fs_v_pfc_right_transitive_first_productcoefficientscoefficientsum) + (pfc_natural_sum_right_transitive_first_productcoefficientscoefficient))) /\ forall fs_i_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps = S (pfc_index_right_transitive_first_productcoefficients)) -> exists fs_a_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps fs_r_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps fs_s_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_transitive_first_productcoefficientscoefficient)) /\ exists fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_right_transitive_first_productcoefficientscoefficient = fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_transitive_first_productcoefficientscoefficient) + (fs_a_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_first_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_right_transitive_first_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_first_productcoefficientscoefficientsum) + (fs_r_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_first_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_right_transitive_first_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_first_productcoefficientscoefficientsum) + (fs_s_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps = fs_r_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps + fs_a_pfc_right_transitive_first_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_right_transitive_first_productcoefficientscoefficientresiduebound. pfa_gap_right_transitive_first_productcoefficientscoefficientresiduebound + S (pfc_value_right_transitive_first_productcoefficients) = (p)) /\ ((exists pfa_offset_left_right_transitive_first_productcoefficientscoefficientresiduecongruence pfa_offset_right_right_transitive_first_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_right_transitive_first_productcoefficientscoefficient) + (p) * pfa_offset_left_right_transitive_first_productcoefficientscoefficientresiduecongruence = (pfc_value_right_transitive_first_productcoefficients) + (p) * pfa_offset_right_right_transitive_first_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_right_transitive_first_target pfrep_left_right_transitive_first_target pfrep_right_right_transitive_first_target. ((exists pfrep_position_right_transitive_first_targetfirst. ((pfrep_position_right_transitive_first_targetfirst+S (pfrep_power_right_transitive_first_target)=(pfrd_plen_right_transitive_first)) /\ ((((exists ff_h_pfp_right_transitive_first_targetfirstentry. ff_h_pfp_right_transitive_first_targetfirstentry + S (pfrep_left_right_transitive_first_target) = S ((S (pfrep_position_right_transitive_first_targetfirst)) * pfrd_pc_right_transitive_first)) /\ exists ff_q_pfp_right_transitive_first_targetfirstentry. pfrd_pb_right_transitive_first = ff_q_pfp_right_transitive_first_targetfirstentry * S ((S (pfrep_position_right_transitive_first_targetfirst)) * pfrd_pc_right_transitive_first) + (pfrep_left_right_transitive_first_target)))))) \/ (((exists pfrep_gap_right_transitive_first_targetfirstoutside. pfrep_gap_right_transitive_first_targetfirstoutside+(pfrd_plen_right_transitive_first)=(pfrep_power_right_transitive_first_target)) /\ (((pfrep_left_right_transitive_first_target)=0))))) -> ((exists pfrep_position_right_transitive_first_targetsecond. ((pfrep_position_right_transitive_first_targetsecond+S (pfrep_power_right_transitive_first_target)=(L)) /\ ((((exists ff_h_pfp_right_transitive_first_targetsecondentry. ff_h_pfp_right_transitive_first_targetsecondentry + S (pfrep_right_right_transitive_first_target) = S ((S (pfrep_position_right_transitive_first_targetsecond)) * ac)) /\ exists ff_q_pfp_right_transitive_first_targetsecondentry. ab = ff_q_pfp_right_transitive_first_targetsecondentry * S ((S (pfrep_position_right_transitive_first_targetsecond)) * ac) + (pfrep_right_right_transitive_first_target)))))) \/ (((exists pfrep_gap_right_transitive_first_targetsecondoutside. pfrep_gap_right_transitive_first_targetsecondoutside+(L)=(pfrep_power_right_transitive_first_target)) /\ (((pfrep_right_right_transitive_first_target)=0))))) -> pfrep_left_right_transitive_first_target=pfrep_right_right_transitive_first_target))))))) -> (((forall fom_index_pfp_right_transitive_second_canonical. (exists fom_gap_pfp_right_transitive_second_canonical_index_bound. fom_gap_pfp_right_transitive_second_canonical_index_bound + S (fom_index_pfp_right_transitive_second_canonical) = M) -> exists fom_value_pfp_right_transitive_second_canonical. ((((exists fom_beta_height_pfp_right_transitive_second_canonical_entry. fom_beta_height_pfp_right_transitive_second_canonical_entry + S (fom_value_pfp_right_transitive_second_canonical) = S ((S (fom_index_pfp_right_transitive_second_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_right_transitive_second_canonical_entry. bb = fom_beta_quotient_pfp_right_transitive_second_canonical_entry * S ((S (fom_index_pfp_right_transitive_second_canonical)) * bc) + (fom_value_pfp_right_transitive_second_canonical))) /\ (exists fom_gap_pfp_right_transitive_second_canonical_value_bound. fom_gap_pfp_right_transitive_second_canonical_value_bound + S (fom_value_pfp_right_transitive_second_canonical) = p))) /\ ((exists pfrd_qb_right_transitive_second pfrd_qc_right_transitive_second pfrd_qlen_right_transitive_second pfrd_pb_right_transitive_second pfrd_pc_right_transitive_second pfrd_plen_right_transitive_second. ((((forall fom_index_pfp_right_transitive_second_productleft. (exists fom_gap_pfp_right_transitive_second_productleft_index_bound. fom_gap_pfp_right_transitive_second_productleft_index_bound + S (fom_index_pfp_right_transitive_second_productleft) = pfrd_qlen_right_transitive_second) -> exists fom_value_pfp_right_transitive_second_productleft. ((((exists fom_beta_height_pfp_right_transitive_second_productleft_entry. fom_beta_height_pfp_right_transitive_second_productleft_entry + S (fom_value_pfp_right_transitive_second_productleft) = S ((S (fom_index_pfp_right_transitive_second_productleft)) * pfrd_qc_right_transitive_second)) /\ exists fom_beta_quotient_pfp_right_transitive_second_productleft_entry. pfrd_qb_right_transitive_second = fom_beta_quotient_pfp_right_transitive_second_productleft_entry * S ((S (fom_index_pfp_right_transitive_second_productleft)) * pfrd_qc_right_transitive_second) + (fom_value_pfp_right_transitive_second_productleft))) /\ (exists fom_gap_pfp_right_transitive_second_productleft_value_bound. fom_gap_pfp_right_transitive_second_productleft_value_bound + S (fom_value_pfp_right_transitive_second_productleft) = p))) /\ (((forall fom_index_pfp_right_transitive_second_productright. (exists fom_gap_pfp_right_transitive_second_productright_index_bound. fom_gap_pfp_right_transitive_second_productright_index_bound + S (fom_index_pfp_right_transitive_second_productright) = L) -> exists fom_value_pfp_right_transitive_second_productright. ((((exists fom_beta_height_pfp_right_transitive_second_productright_entry. fom_beta_height_pfp_right_transitive_second_productright_entry + S (fom_value_pfp_right_transitive_second_productright) = S ((S (fom_index_pfp_right_transitive_second_productright)) * ac)) /\ exists fom_beta_quotient_pfp_right_transitive_second_productright_entry. ab = fom_beta_quotient_pfp_right_transitive_second_productright_entry * S ((S (fom_index_pfp_right_transitive_second_productright)) * ac) + (fom_value_pfp_right_transitive_second_productright))) /\ (exists fom_gap_pfp_right_transitive_second_productright_value_bound. fom_gap_pfp_right_transitive_second_productright_value_bound + S (fom_value_pfp_right_transitive_second_productright) = p))) /\ (((((((pfrd_qlen_right_transitive_second)=0 \/ (L)=0) /\ (((pfrd_plen_right_transitive_second)=0)))) \/ (((~((pfrd_qlen_right_transitive_second)=0)) /\ (((~((L)=0)) /\ (((pfrd_qlen_right_transitive_second)+(L)=S (pfrd_plen_right_transitive_second)))))))) /\ ((forall pfc_index_right_transitive_second_productcoefficients. (exists pfa_gap_right_transitive_second_productcoefficientsbound. pfa_gap_right_transitive_second_productcoefficientsbound + S (pfc_index_right_transitive_second_productcoefficients) = (pfrd_plen_right_transitive_second)) -> exists pfc_value_right_transitive_second_productcoefficients. ((((exists ff_h_pfp_right_transitive_second_productcoefficientsentry. ff_h_pfp_right_transitive_second_productcoefficientsentry + S (pfc_value_right_transitive_second_productcoefficients) = S ((S (pfc_index_right_transitive_second_productcoefficients)) * pfrd_pc_right_transitive_second)) /\ exists ff_q_pfp_right_transitive_second_productcoefficientsentry. pfrd_pb_right_transitive_second = ff_q_pfp_right_transitive_second_productcoefficientsentry * S ((S (pfc_index_right_transitive_second_productcoefficients)) * pfrd_pc_right_transitive_second) + (pfc_value_right_transitive_second_productcoefficients))) /\ ((exists pfc_terms_code_right_transitive_second_productcoefficientscoefficient pfc_terms_scale_right_transitive_second_productcoefficientscoefficient pfc_natural_sum_right_transitive_second_productcoefficientscoefficient. ((forall pfc_index_right_transitive_second_productcoefficientscoefficientdiagonal. (exists pfa_gap_right_transitive_second_productcoefficientscoefficientdiagonalbound. pfa_gap_right_transitive_second_productcoefficientscoefficientdiagonalbound + S (pfc_index_right_transitive_second_productcoefficientscoefficientdiagonal) = (S (pfc_index_right_transitive_second_productcoefficients))) -> exists pfc_value_right_transitive_second_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_right_transitive_second_productcoefficientscoefficientdiagonalentry. ff_h_pfp_right_transitive_second_productcoefficientscoefficientdiagonalentry + S (pfc_value_right_transitive_second_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_right_transitive_second_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_transitive_second_productcoefficientscoefficient)) /\ exists ff_q_pfp_right_transitive_second_productcoefficientscoefficientdiagonalentry. pfc_terms_code_right_transitive_second_productcoefficientscoefficient = ff_q_pfp_right_transitive_second_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_right_transitive_second_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_transitive_second_productcoefficientscoefficient) + (pfc_value_right_transitive_second_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_right_transitive_second_productcoefficientscoefficientdiagonalterm pfc_left_right_transitive_second_productcoefficientscoefficientdiagonalterm pfc_right_right_transitive_second_productcoefficientscoefficientdiagonalterm. (((pfc_index_right_transitive_second_productcoefficientscoefficientdiagonal)+pfc_complement_right_transitive_second_productcoefficientscoefficientdiagonalterm=(pfc_index_right_transitive_second_productcoefficients)) /\ ((((((exists pfa_gap_right_transitive_second_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_right_transitive_second_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_right_transitive_second_productcoefficientscoefficientdiagonal) = (pfrd_qlen_right_transitive_second)) /\ ((((exists ff_h_pfp_right_transitive_second_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_right_transitive_second_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_right_transitive_second_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_right_transitive_second_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_transitive_second)) /\ exists ff_q_pfp_right_transitive_second_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_right_transitive_second = ff_q_pfp_right_transitive_second_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_right_transitive_second_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_transitive_second) + (pfc_left_right_transitive_second_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_transitive_second_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_right_transitive_second_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_right_transitive_second)=(pfc_index_right_transitive_second_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_right_transitive_second_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_right_transitive_second_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_right_transitive_second_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_right_transitive_second_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_right_transitive_second_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_right_transitive_second_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_right_transitive_second_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_right_transitive_second_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_right_transitive_second_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_right_transitive_second_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_right_transitive_second_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_right_transitive_second_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_transitive_second_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_right_transitive_second_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_right_transitive_second_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_right_transitive_second_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_right_transitive_second_productcoefficientscoefficientdiagonal)=pfc_left_right_transitive_second_productcoefficientscoefficientdiagonalterm*pfc_right_right_transitive_second_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_right_transitive_second_productcoefficientscoefficientsum fs_v_pfc_right_transitive_second_productcoefficientscoefficientsum. ((((exists fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_start. fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_right_transitive_second_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_start. fs_u_pfc_right_transitive_second_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_right_transitive_second_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_right_transitive_second_productcoefficientscoefficient) = S ((S (S (pfc_index_right_transitive_second_productcoefficients))) * fs_v_pfc_right_transitive_second_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_right_transitive_second_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_right_transitive_second_productcoefficients))) * fs_v_pfc_right_transitive_second_productcoefficientscoefficientsum) + (pfc_natural_sum_right_transitive_second_productcoefficientscoefficient))) /\ forall fs_i_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps = S (pfc_index_right_transitive_second_productcoefficients)) -> exists fs_a_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps fs_r_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps fs_s_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_transitive_second_productcoefficientscoefficient)) /\ exists fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_right_transitive_second_productcoefficientscoefficient = fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_transitive_second_productcoefficientscoefficient) + (fs_a_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_second_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_right_transitive_second_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_second_productcoefficientscoefficientsum) + (fs_r_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_second_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_right_transitive_second_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_second_productcoefficientscoefficientsum) + (fs_s_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps = fs_r_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps + fs_a_pfc_right_transitive_second_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_right_transitive_second_productcoefficientscoefficientresiduebound. pfa_gap_right_transitive_second_productcoefficientscoefficientresiduebound + S (pfc_value_right_transitive_second_productcoefficients) = (p)) /\ ((exists pfa_offset_left_right_transitive_second_productcoefficientscoefficientresiduecongruence pfa_offset_right_right_transitive_second_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_right_transitive_second_productcoefficientscoefficient) + (p) * pfa_offset_left_right_transitive_second_productcoefficientscoefficientresiduecongruence = (pfc_value_right_transitive_second_productcoefficients) + (p) * pfa_offset_right_right_transitive_second_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_right_transitive_second_target pfrep_left_right_transitive_second_target pfrep_right_right_transitive_second_target. ((exists pfrep_position_right_transitive_second_targetfirst. ((pfrep_position_right_transitive_second_targetfirst+S (pfrep_power_right_transitive_second_target)=(pfrd_plen_right_transitive_second)) /\ ((((exists ff_h_pfp_right_transitive_second_targetfirstentry. ff_h_pfp_right_transitive_second_targetfirstentry + S (pfrep_left_right_transitive_second_target) = S ((S (pfrep_position_right_transitive_second_targetfirst)) * pfrd_pc_right_transitive_second)) /\ exists ff_q_pfp_right_transitive_second_targetfirstentry. pfrd_pb_right_transitive_second = ff_q_pfp_right_transitive_second_targetfirstentry * S ((S (pfrep_position_right_transitive_second_targetfirst)) * pfrd_pc_right_transitive_second) + (pfrep_left_right_transitive_second_target)))))) \/ (((exists pfrep_gap_right_transitive_second_targetfirstoutside. pfrep_gap_right_transitive_second_targetfirstoutside+(pfrd_plen_right_transitive_second)=(pfrep_power_right_transitive_second_target)) /\ (((pfrep_left_right_transitive_second_target)=0))))) -> ((exists pfrep_position_right_transitive_second_targetsecond. ((pfrep_position_right_transitive_second_targetsecond+S (pfrep_power_right_transitive_second_target)=(M)) /\ ((((exists ff_h_pfp_right_transitive_second_targetsecondentry. ff_h_pfp_right_transitive_second_targetsecondentry + S (pfrep_right_right_transitive_second_target) = S ((S (pfrep_position_right_transitive_second_targetsecond)) * bc)) /\ exists ff_q_pfp_right_transitive_second_targetsecondentry. bb = ff_q_pfp_right_transitive_second_targetsecondentry * S ((S (pfrep_position_right_transitive_second_targetsecond)) * bc) + (pfrep_right_right_transitive_second_target)))))) \/ (((exists pfrep_gap_right_transitive_second_targetsecondoutside. pfrep_gap_right_transitive_second_targetsecondoutside+(M)=(pfrep_power_right_transitive_second_target)) /\ (((pfrep_right_right_transitive_second_target)=0))))) -> pfrep_left_right_transitive_second_target=pfrep_right_right_transitive_second_target))))))) -> (((forall fom_index_pfp_right_transitive_result_canonical. (exists fom_gap_pfp_right_transitive_result_canonical_index_bound. fom_gap_pfp_right_transitive_result_canonical_index_bound + S (fom_index_pfp_right_transitive_result_canonical) = M) -> exists fom_value_pfp_right_transitive_result_canonical. ((((exists fom_beta_height_pfp_right_transitive_result_canonical_entry. fom_beta_height_pfp_right_transitive_result_canonical_entry + S (fom_value_pfp_right_transitive_result_canonical) = S ((S (fom_index_pfp_right_transitive_result_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_right_transitive_result_canonical_entry. bb = fom_beta_quotient_pfp_right_transitive_result_canonical_entry * S ((S (fom_index_pfp_right_transitive_result_canonical)) * bc) + (fom_value_pfp_right_transitive_result_canonical))) /\ (exists fom_gap_pfp_right_transitive_result_canonical_value_bound. fom_gap_pfp_right_transitive_result_canonical_value_bound + S (fom_value_pfp_right_transitive_result_canonical) = p))) /\ ((exists pfrd_qb_right_transitive_result pfrd_qc_right_transitive_result pfrd_qlen_right_transitive_result pfrd_pb_right_transitive_result pfrd_pc_right_transitive_result pfrd_plen_right_transitive_result. ((((forall fom_index_pfp_right_transitive_result_productleft. (exists fom_gap_pfp_right_transitive_result_productleft_index_bound. fom_gap_pfp_right_transitive_result_productleft_index_bound + S (fom_index_pfp_right_transitive_result_productleft) = pfrd_qlen_right_transitive_result) -> exists fom_value_pfp_right_transitive_result_productleft. ((((exists fom_beta_height_pfp_right_transitive_result_productleft_entry. fom_beta_height_pfp_right_transitive_result_productleft_entry + S (fom_value_pfp_right_transitive_result_productleft) = S ((S (fom_index_pfp_right_transitive_result_productleft)) * pfrd_qc_right_transitive_result)) /\ exists fom_beta_quotient_pfp_right_transitive_result_productleft_entry. pfrd_qb_right_transitive_result = fom_beta_quotient_pfp_right_transitive_result_productleft_entry * S ((S (fom_index_pfp_right_transitive_result_productleft)) * pfrd_qc_right_transitive_result) + (fom_value_pfp_right_transitive_result_productleft))) /\ (exists fom_gap_pfp_right_transitive_result_productleft_value_bound. fom_gap_pfp_right_transitive_result_productleft_value_bound + S (fom_value_pfp_right_transitive_result_productleft) = p))) /\ (((forall fom_index_pfp_right_transitive_result_productright. (exists fom_gap_pfp_right_transitive_result_productright_index_bound. fom_gap_pfp_right_transitive_result_productright_index_bound + S (fom_index_pfp_right_transitive_result_productright) = D) -> exists fom_value_pfp_right_transitive_result_productright. ((((exists fom_beta_height_pfp_right_transitive_result_productright_entry. fom_beta_height_pfp_right_transitive_result_productright_entry + S (fom_value_pfp_right_transitive_result_productright) = S ((S (fom_index_pfp_right_transitive_result_productright)) * dc)) /\ exists fom_beta_quotient_pfp_right_transitive_result_productright_entry. db = fom_beta_quotient_pfp_right_transitive_result_productright_entry * S ((S (fom_index_pfp_right_transitive_result_productright)) * dc) + (fom_value_pfp_right_transitive_result_productright))) /\ (exists fom_gap_pfp_right_transitive_result_productright_value_bound. fom_gap_pfp_right_transitive_result_productright_value_bound + S (fom_value_pfp_right_transitive_result_productright) = p))) /\ (((((((pfrd_qlen_right_transitive_result)=0 \/ (D)=0) /\ (((pfrd_plen_right_transitive_result)=0)))) \/ (((~((pfrd_qlen_right_transitive_result)=0)) /\ (((~((D)=0)) /\ (((pfrd_qlen_right_transitive_result)+(D)=S (pfrd_plen_right_transitive_result)))))))) /\ ((forall pfc_index_right_transitive_result_productcoefficients. (exists pfa_gap_right_transitive_result_productcoefficientsbound. pfa_gap_right_transitive_result_productcoefficientsbound + S (pfc_index_right_transitive_result_productcoefficients) = (pfrd_plen_right_transitive_result)) -> exists pfc_value_right_transitive_result_productcoefficients. ((((exists ff_h_pfp_right_transitive_result_productcoefficientsentry. ff_h_pfp_right_transitive_result_productcoefficientsentry + S (pfc_value_right_transitive_result_productcoefficients) = S ((S (pfc_index_right_transitive_result_productcoefficients)) * pfrd_pc_right_transitive_result)) /\ exists ff_q_pfp_right_transitive_result_productcoefficientsentry. pfrd_pb_right_transitive_result = ff_q_pfp_right_transitive_result_productcoefficientsentry * S ((S (pfc_index_right_transitive_result_productcoefficients)) * pfrd_pc_right_transitive_result) + (pfc_value_right_transitive_result_productcoefficients))) /\ ((exists pfc_terms_code_right_transitive_result_productcoefficientscoefficient pfc_terms_scale_right_transitive_result_productcoefficientscoefficient pfc_natural_sum_right_transitive_result_productcoefficientscoefficient. ((forall pfc_index_right_transitive_result_productcoefficientscoefficientdiagonal. (exists pfa_gap_right_transitive_result_productcoefficientscoefficientdiagonalbound. pfa_gap_right_transitive_result_productcoefficientscoefficientdiagonalbound + S (pfc_index_right_transitive_result_productcoefficientscoefficientdiagonal) = (S (pfc_index_right_transitive_result_productcoefficients))) -> exists pfc_value_right_transitive_result_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_right_transitive_result_productcoefficientscoefficientdiagonalentry. ff_h_pfp_right_transitive_result_productcoefficientscoefficientdiagonalentry + S (pfc_value_right_transitive_result_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_right_transitive_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_transitive_result_productcoefficientscoefficient)) /\ exists ff_q_pfp_right_transitive_result_productcoefficientscoefficientdiagonalentry. pfc_terms_code_right_transitive_result_productcoefficientscoefficient = ff_q_pfp_right_transitive_result_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_right_transitive_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_transitive_result_productcoefficientscoefficient) + (pfc_value_right_transitive_result_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_right_transitive_result_productcoefficientscoefficientdiagonalterm pfc_left_right_transitive_result_productcoefficientscoefficientdiagonalterm pfc_right_right_transitive_result_productcoefficientscoefficientdiagonalterm. (((pfc_index_right_transitive_result_productcoefficientscoefficientdiagonal)+pfc_complement_right_transitive_result_productcoefficientscoefficientdiagonalterm=(pfc_index_right_transitive_result_productcoefficients)) /\ ((((((exists pfa_gap_right_transitive_result_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_right_transitive_result_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_right_transitive_result_productcoefficientscoefficientdiagonal) = (pfrd_qlen_right_transitive_result)) /\ ((((exists ff_h_pfp_right_transitive_result_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_right_transitive_result_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_right_transitive_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_right_transitive_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_transitive_result)) /\ exists ff_q_pfp_right_transitive_result_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_right_transitive_result = ff_q_pfp_right_transitive_result_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_right_transitive_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_transitive_result) + (pfc_left_right_transitive_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_transitive_result_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_right_transitive_result_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_right_transitive_result)=(pfc_index_right_transitive_result_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_right_transitive_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_right_transitive_result_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_right_transitive_result_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_right_transitive_result_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_right_transitive_result_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_right_transitive_result_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_right_transitive_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_right_transitive_result_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_right_transitive_result_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_right_transitive_result_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_right_transitive_result_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_right_transitive_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_transitive_result_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_right_transitive_result_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_right_transitive_result_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_right_transitive_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_right_transitive_result_productcoefficientscoefficientdiagonal)=pfc_left_right_transitive_result_productcoefficientscoefficientdiagonalterm*pfc_right_right_transitive_result_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_right_transitive_result_productcoefficientscoefficientsum fs_v_pfc_right_transitive_result_productcoefficientscoefficientsum. ((((exists fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_start. fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_right_transitive_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_start. fs_u_pfc_right_transitive_result_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_right_transitive_result_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_right_transitive_result_productcoefficientscoefficient) = S ((S (S (pfc_index_right_transitive_result_productcoefficients))) * fs_v_pfc_right_transitive_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_right_transitive_result_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_right_transitive_result_productcoefficients))) * fs_v_pfc_right_transitive_result_productcoefficientscoefficientsum) + (pfc_natural_sum_right_transitive_result_productcoefficientscoefficient))) /\ forall fs_i_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps = S (pfc_index_right_transitive_result_productcoefficients)) -> exists fs_a_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps fs_r_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps fs_s_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_transitive_result_productcoefficientscoefficient)) /\ exists fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_right_transitive_result_productcoefficientscoefficient = fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_transitive_result_productcoefficientscoefficient) + (fs_a_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_right_transitive_result_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_result_productcoefficientscoefficientsum) + (fs_r_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_right_transitive_result_productcoefficientscoefficientsum = fs_q_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_transitive_result_productcoefficientscoefficientsum) + (fs_s_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps = fs_r_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps + fs_a_pfc_right_transitive_result_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_right_transitive_result_productcoefficientscoefficientresiduebound. pfa_gap_right_transitive_result_productcoefficientscoefficientresiduebound + S (pfc_value_right_transitive_result_productcoefficients) = (p)) /\ ((exists pfa_offset_left_right_transitive_result_productcoefficientscoefficientresiduecongruence pfa_offset_right_right_transitive_result_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_right_transitive_result_productcoefficientscoefficient) + (p) * pfa_offset_left_right_transitive_result_productcoefficientscoefficientresiduecongruence = (pfc_value_right_transitive_result_productcoefficients) + (p) * pfa_offset_right_right_transitive_result_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_right_transitive_result_target pfrep_left_right_transitive_result_target pfrep_right_right_transitive_result_target. ((exists pfrep_position_right_transitive_result_targetfirst. ((pfrep_position_right_transitive_result_targetfirst+S (pfrep_power_right_transitive_result_target)=(pfrd_plen_right_transitive_result)) /\ ((((exists ff_h_pfp_right_transitive_result_targetfirstentry. ff_h_pfp_right_transitive_result_targetfirstentry + S (pfrep_left_right_transitive_result_target) = S ((S (pfrep_position_right_transitive_result_targetfirst)) * pfrd_pc_right_transitive_result)) /\ exists ff_q_pfp_right_transitive_result_targetfirstentry. pfrd_pb_right_transitive_result = ff_q_pfp_right_transitive_result_targetfirstentry * S ((S (pfrep_position_right_transitive_result_targetfirst)) * pfrd_pc_right_transitive_result) + (pfrep_left_right_transitive_result_target)))))) \/ (((exists pfrep_gap_right_transitive_result_targetfirstoutside. pfrep_gap_right_transitive_result_targetfirstoutside+(pfrd_plen_right_transitive_result)=(pfrep_power_right_transitive_result_target)) /\ (((pfrep_left_right_transitive_result_target)=0))))) -> ((exists pfrep_position_right_transitive_result_targetsecond. ((pfrep_position_right_transitive_result_targetsecond+S (pfrep_power_right_transitive_result_target)=(M)) /\ ((((exists ff_h_pfp_right_transitive_result_targetsecondentry. ff_h_pfp_right_transitive_result_targetsecondentry + S (pfrep_right_right_transitive_result_target) = S ((S (pfrep_position_right_transitive_result_targetsecond)) * bc)) /\ exists ff_q_pfp_right_transitive_result_targetsecondentry. bb = ff_q_pfp_right_transitive_result_targetsecondentry * S ((S (pfrep_position_right_transitive_result_targetsecond)) * bc) + (pfrep_right_right_transitive_result_target)))))) \/ (((exists pfrep_gap_right_transitive_result_targetsecondoutside. pfrep_gap_right_transitive_result_targetsecondoutside+(M)=(pfrep_power_right_transitive_result_target)) /\ (((pfrep_right_right_transitive_result_target)=0))))) -> pfrep_left_right_transitive_result_target=pfrep_right_right_transitive_result_target)))))))