prime_field_polynomial_normalized_right_associate_exists

Exact expanded first-order arithmetic statement

forall p ab ac L. (~((p) = 1) /\ forall pfa_factor_left_normalized_associate_prime pfa_factor_right_normalized_associate_prime. (p) = pfa_factor_left_normalized_associate_prime * pfa_factor_right_normalized_associate_prime -> pfa_factor_left_normalized_associate_prime = 1 \/ pfa_factor_right_normalized_associate_prime = 1) -> (forall fom_index_pfp_normalized_associate_input. (exists fom_gap_pfp_normalized_associate_input_index_bound. fom_gap_pfp_normalized_associate_input_index_bound + S (fom_index_pfp_normalized_associate_input) = L) -> exists fom_value_pfp_normalized_associate_input. ((((exists fom_beta_height_pfp_normalized_associate_input_entry. fom_beta_height_pfp_normalized_associate_input_entry + S (fom_value_pfp_normalized_associate_input) = S ((S (fom_index_pfp_normalized_associate_input)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_associate_input_entry. ab = fom_beta_quotient_pfp_normalized_associate_input_entry * S ((S (fom_index_pfp_normalized_associate_input)) * ac) + (fom_value_pfp_normalized_associate_input))) /\ (exists fom_gap_pfp_normalized_associate_input_value_bound. fom_gap_pfp_normalized_associate_input_value_bound + S (fom_value_pfp_normalized_associate_input) = p))) -> (exists hb hc H. ((H=0 \/ (((~((H) = 0)) /\ (((forall fom_index_pfp_normalized_associate_result_moniccoefficients. (exists fom_gap_pfp_normalized_associate_result_moniccoefficients_index_bound. fom_gap_pfp_normalized_associate_result_moniccoefficients_index_bound + S (fom_index_pfp_normalized_associate_result_moniccoefficients) = H) -> exists fom_value_pfp_normalized_associate_result_moniccoefficients. ((((exists fom_beta_height_pfp_normalized_associate_result_moniccoefficients_entry. fom_beta_height_pfp_normalized_associate_result_moniccoefficients_entry + S (fom_value_pfp_normalized_associate_result_moniccoefficients) = S ((S (fom_index_pfp_normalized_associate_result_moniccoefficients)) * hc)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_moniccoefficients_entry. hb = fom_beta_quotient_pfp_normalized_associate_result_moniccoefficients_entry * S ((S (fom_index_pfp_normalized_associate_result_moniccoefficients)) * hc) + (fom_value_pfp_normalized_associate_result_moniccoefficients))) /\ (exists fom_gap_pfp_normalized_associate_result_moniccoefficients_value_bound. fom_gap_pfp_normalized_associate_result_moniccoefficients_value_bound + S (fom_value_pfp_normalized_associate_result_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_normalized_associate_result_monicleading. ff_h_pfp_normalized_associate_result_monicleading + S (1) = S ((S (0)) * hc)) /\ exists ff_q_pfp_normalized_associate_result_monicleading. hb = ff_q_pfp_normalized_associate_result_monicleading * S ((S (0)) * hc) + (1))))))))) /\ (((((forall fom_index_pfp_normalized_associate_result_forward_canonical. (exists fom_gap_pfp_normalized_associate_result_forward_canonical_index_bound. fom_gap_pfp_normalized_associate_result_forward_canonical_index_bound + S (fom_index_pfp_normalized_associate_result_forward_canonical) = H) -> exists fom_value_pfp_normalized_associate_result_forward_canonical. ((((exists fom_beta_height_pfp_normalized_associate_result_forward_canonical_entry. fom_beta_height_pfp_normalized_associate_result_forward_canonical_entry + S (fom_value_pfp_normalized_associate_result_forward_canonical) = S ((S (fom_index_pfp_normalized_associate_result_forward_canonical)) * hc)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_forward_canonical_entry. hb = fom_beta_quotient_pfp_normalized_associate_result_forward_canonical_entry * S ((S (fom_index_pfp_normalized_associate_result_forward_canonical)) * hc) + (fom_value_pfp_normalized_associate_result_forward_canonical))) /\ (exists fom_gap_pfp_normalized_associate_result_forward_canonical_value_bound. fom_gap_pfp_normalized_associate_result_forward_canonical_value_bound + S (fom_value_pfp_normalized_associate_result_forward_canonical) = p))) /\ ((exists pfen_qb_normalized_associate_result_forward pfen_qc_normalized_associate_result_forward pfen_qlen_normalized_associate_result_forward pfen_pb_normalized_associate_result_forward pfen_pc_normalized_associate_result_forward pfen_plen_normalized_associate_result_forward. ((((forall fom_index_pfp_normalized_associate_result_forward_productleft. (exists fom_gap_pfp_normalized_associate_result_forward_productleft_index_bound. fom_gap_pfp_normalized_associate_result_forward_productleft_index_bound + S (fom_index_pfp_normalized_associate_result_forward_productleft) = pfen_qlen_normalized_associate_result_forward) -> exists fom_value_pfp_normalized_associate_result_forward_productleft. ((((exists fom_beta_height_pfp_normalized_associate_result_forward_productleft_entry. fom_beta_height_pfp_normalized_associate_result_forward_productleft_entry + S (fom_value_pfp_normalized_associate_result_forward_productleft) = S ((S (fom_index_pfp_normalized_associate_result_forward_productleft)) * pfen_qc_normalized_associate_result_forward)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_forward_productleft_entry. pfen_qb_normalized_associate_result_forward = fom_beta_quotient_pfp_normalized_associate_result_forward_productleft_entry * S ((S (fom_index_pfp_normalized_associate_result_forward_productleft)) * pfen_qc_normalized_associate_result_forward) + (fom_value_pfp_normalized_associate_result_forward_productleft))) /\ (exists fom_gap_pfp_normalized_associate_result_forward_productleft_value_bound. fom_gap_pfp_normalized_associate_result_forward_productleft_value_bound + S (fom_value_pfp_normalized_associate_result_forward_productleft) = p))) /\ (((forall fom_index_pfp_normalized_associate_result_forward_productright. (exists fom_gap_pfp_normalized_associate_result_forward_productright_index_bound. fom_gap_pfp_normalized_associate_result_forward_productright_index_bound + S (fom_index_pfp_normalized_associate_result_forward_productright) = L) -> exists fom_value_pfp_normalized_associate_result_forward_productright. ((((exists fom_beta_height_pfp_normalized_associate_result_forward_productright_entry. fom_beta_height_pfp_normalized_associate_result_forward_productright_entry + S (fom_value_pfp_normalized_associate_result_forward_productright) = S ((S (fom_index_pfp_normalized_associate_result_forward_productright)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_forward_productright_entry. ab = fom_beta_quotient_pfp_normalized_associate_result_forward_productright_entry * S ((S (fom_index_pfp_normalized_associate_result_forward_productright)) * ac) + (fom_value_pfp_normalized_associate_result_forward_productright))) /\ (exists fom_gap_pfp_normalized_associate_result_forward_productright_value_bound. fom_gap_pfp_normalized_associate_result_forward_productright_value_bound + S (fom_value_pfp_normalized_associate_result_forward_productright) = p))) /\ (((((((pfen_qlen_normalized_associate_result_forward)=0 \/ (L)=0) /\ (((pfen_plen_normalized_associate_result_forward)=0)))) \/ (((~((pfen_qlen_normalized_associate_result_forward)=0)) /\ (((~((L)=0)) /\ (((pfen_qlen_normalized_associate_result_forward)+(L)=S (pfen_plen_normalized_associate_result_forward)))))))) /\ ((forall pfc_index_normalized_associate_result_forward_productcoefficients. (exists pfa_gap_normalized_associate_result_forward_productcoefficientsbound. pfa_gap_normalized_associate_result_forward_productcoefficientsbound + S (pfc_index_normalized_associate_result_forward_productcoefficients) = (pfen_plen_normalized_associate_result_forward)) -> exists pfc_value_normalized_associate_result_forward_productcoefficients. ((((exists ff_h_pfp_normalized_associate_result_forward_productcoefficientsentry. ff_h_pfp_normalized_associate_result_forward_productcoefficientsentry + S (pfc_value_normalized_associate_result_forward_productcoefficients) = S ((S (pfc_index_normalized_associate_result_forward_productcoefficients)) * pfen_pc_normalized_associate_result_forward)) /\ exists ff_q_pfp_normalized_associate_result_forward_productcoefficientsentry. pfen_pb_normalized_associate_result_forward = ff_q_pfp_normalized_associate_result_forward_productcoefficientsentry * S ((S (pfc_index_normalized_associate_result_forward_productcoefficients)) * pfen_pc_normalized_associate_result_forward) + (pfc_value_normalized_associate_result_forward_productcoefficients))) /\ ((exists pfc_terms_code_normalized_associate_result_forward_productcoefficientscoefficient pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient pfc_natural_sum_normalized_associate_result_forward_productcoefficientscoefficient. ((forall pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonalbound. pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_associate_result_forward_productcoefficients))) -> exists pfc_value_normalized_associate_result_forward_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_associate_result_forward_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_associate_result_forward_productcoefficientscoefficient = ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient) + (pfc_value_normalized_associate_result_forward_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)+pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm=(pfc_index_normalized_associate_result_forward_productcoefficients)) /\ ((((((exists pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal) = (pfen_qlen_normalized_associate_result_forward)) /\ ((((exists ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalized_associate_result_forward)) /\ exists ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftentry. pfen_qb_normalized_associate_result_forward = ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalized_associate_result_forward) + (pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermleftoutside+(pfen_qlen_normalized_associate_result_forward)=(pfc_index_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_associate_result_forward_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_associate_result_forward_productcoefficientscoefficientdiagonal)=pfc_left_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm*pfc_right_normalized_associate_result_forward_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_associate_result_forward_productcoefficientscoefficient) = S ((S (S (pfc_index_normalized_associate_result_forward_productcoefficients))) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_associate_result_forward_productcoefficients))) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum) + (pfc_natural_sum_normalized_associate_result_forward_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_associate_result_forward_productcoefficients)) -> exists fs_a_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_associate_result_forward_productcoefficientscoefficient = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_associate_result_forward_productcoefficientscoefficient) + (fs_a_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum) + (fs_r_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum) + (fs_s_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_associate_result_forward_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientresiduebound. pfa_gap_normalized_associate_result_forward_productcoefficientscoefficientresiduebound + S (pfc_value_normalized_associate_result_forward_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_associate_result_forward_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_associate_result_forward_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_associate_result_forward_productcoefficientscoefficient) + (p) * pfa_offset_left_normalized_associate_result_forward_productcoefficientscoefficientresiduecongruence = (pfc_value_normalized_associate_result_forward_productcoefficients) + (p) * pfa_offset_right_normalized_associate_result_forward_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalized_associate_result_forward_target pfrep_left_normalized_associate_result_forward_target pfrep_right_normalized_associate_result_forward_target. ((exists pfrep_position_normalized_associate_result_forward_targetfirst. ((pfrep_position_normalized_associate_result_forward_targetfirst+S (pfrep_power_normalized_associate_result_forward_target)=(pfen_plen_normalized_associate_result_forward)) /\ ((((exists ff_h_pfp_normalized_associate_result_forward_targetfirstentry. ff_h_pfp_normalized_associate_result_forward_targetfirstentry + S (pfrep_left_normalized_associate_result_forward_target) = S ((S (pfrep_position_normalized_associate_result_forward_targetfirst)) * pfen_pc_normalized_associate_result_forward)) /\ exists ff_q_pfp_normalized_associate_result_forward_targetfirstentry. pfen_pb_normalized_associate_result_forward = ff_q_pfp_normalized_associate_result_forward_targetfirstentry * S ((S (pfrep_position_normalized_associate_result_forward_targetfirst)) * pfen_pc_normalized_associate_result_forward) + (pfrep_left_normalized_associate_result_forward_target)))))) \/ (((exists pfrep_gap_normalized_associate_result_forward_targetfirstoutside. pfrep_gap_normalized_associate_result_forward_targetfirstoutside+(pfen_plen_normalized_associate_result_forward)=(pfrep_power_normalized_associate_result_forward_target)) /\ (((pfrep_left_normalized_associate_result_forward_target)=0))))) -> ((exists pfrep_position_normalized_associate_result_forward_targetsecond. ((pfrep_position_normalized_associate_result_forward_targetsecond+S (pfrep_power_normalized_associate_result_forward_target)=(H)) /\ ((((exists ff_h_pfp_normalized_associate_result_forward_targetsecondentry. ff_h_pfp_normalized_associate_result_forward_targetsecondentry + S (pfrep_right_normalized_associate_result_forward_target) = S ((S (pfrep_position_normalized_associate_result_forward_targetsecond)) * hc)) /\ exists ff_q_pfp_normalized_associate_result_forward_targetsecondentry. hb = ff_q_pfp_normalized_associate_result_forward_targetsecondentry * S ((S (pfrep_position_normalized_associate_result_forward_targetsecond)) * hc) + (pfrep_right_normalized_associate_result_forward_target)))))) \/ (((exists pfrep_gap_normalized_associate_result_forward_targetsecondoutside. pfrep_gap_normalized_associate_result_forward_targetsecondoutside+(H)=(pfrep_power_normalized_associate_result_forward_target)) /\ (((pfrep_right_normalized_associate_result_forward_target)=0))))) -> pfrep_left_normalized_associate_result_forward_target=pfrep_right_normalized_associate_result_forward_target))))))) /\ ((((forall fom_index_pfp_normalized_associate_result_backward_canonical. (exists fom_gap_pfp_normalized_associate_result_backward_canonical_index_bound. fom_gap_pfp_normalized_associate_result_backward_canonical_index_bound + S (fom_index_pfp_normalized_associate_result_backward_canonical) = L) -> exists fom_value_pfp_normalized_associate_result_backward_canonical. ((((exists fom_beta_height_pfp_normalized_associate_result_backward_canonical_entry. fom_beta_height_pfp_normalized_associate_result_backward_canonical_entry + S (fom_value_pfp_normalized_associate_result_backward_canonical) = S ((S (fom_index_pfp_normalized_associate_result_backward_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_backward_canonical_entry. ab = fom_beta_quotient_pfp_normalized_associate_result_backward_canonical_entry * S ((S (fom_index_pfp_normalized_associate_result_backward_canonical)) * ac) + (fom_value_pfp_normalized_associate_result_backward_canonical))) /\ (exists fom_gap_pfp_normalized_associate_result_backward_canonical_value_bound. fom_gap_pfp_normalized_associate_result_backward_canonical_value_bound + S (fom_value_pfp_normalized_associate_result_backward_canonical) = p))) /\ ((exists pfen_qb_normalized_associate_result_backward pfen_qc_normalized_associate_result_backward pfen_qlen_normalized_associate_result_backward pfen_pb_normalized_associate_result_backward pfen_pc_normalized_associate_result_backward pfen_plen_normalized_associate_result_backward. ((((forall fom_index_pfp_normalized_associate_result_backward_productleft. (exists fom_gap_pfp_normalized_associate_result_backward_productleft_index_bound. fom_gap_pfp_normalized_associate_result_backward_productleft_index_bound + S (fom_index_pfp_normalized_associate_result_backward_productleft) = pfen_qlen_normalized_associate_result_backward) -> exists fom_value_pfp_normalized_associate_result_backward_productleft. ((((exists fom_beta_height_pfp_normalized_associate_result_backward_productleft_entry. fom_beta_height_pfp_normalized_associate_result_backward_productleft_entry + S (fom_value_pfp_normalized_associate_result_backward_productleft) = S ((S (fom_index_pfp_normalized_associate_result_backward_productleft)) * pfen_qc_normalized_associate_result_backward)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_backward_productleft_entry. pfen_qb_normalized_associate_result_backward = fom_beta_quotient_pfp_normalized_associate_result_backward_productleft_entry * S ((S (fom_index_pfp_normalized_associate_result_backward_productleft)) * pfen_qc_normalized_associate_result_backward) + (fom_value_pfp_normalized_associate_result_backward_productleft))) /\ (exists fom_gap_pfp_normalized_associate_result_backward_productleft_value_bound. fom_gap_pfp_normalized_associate_result_backward_productleft_value_bound + S (fom_value_pfp_normalized_associate_result_backward_productleft) = p))) /\ (((forall fom_index_pfp_normalized_associate_result_backward_productright. (exists fom_gap_pfp_normalized_associate_result_backward_productright_index_bound. fom_gap_pfp_normalized_associate_result_backward_productright_index_bound + S (fom_index_pfp_normalized_associate_result_backward_productright) = H) -> exists fom_value_pfp_normalized_associate_result_backward_productright. ((((exists fom_beta_height_pfp_normalized_associate_result_backward_productright_entry. fom_beta_height_pfp_normalized_associate_result_backward_productright_entry + S (fom_value_pfp_normalized_associate_result_backward_productright) = S ((S (fom_index_pfp_normalized_associate_result_backward_productright)) * hc)) /\ exists fom_beta_quotient_pfp_normalized_associate_result_backward_productright_entry. hb = fom_beta_quotient_pfp_normalized_associate_result_backward_productright_entry * S ((S (fom_index_pfp_normalized_associate_result_backward_productright)) * hc) + (fom_value_pfp_normalized_associate_result_backward_productright))) /\ (exists fom_gap_pfp_normalized_associate_result_backward_productright_value_bound. fom_gap_pfp_normalized_associate_result_backward_productright_value_bound + S (fom_value_pfp_normalized_associate_result_backward_productright) = p))) /\ (((((((pfen_qlen_normalized_associate_result_backward)=0 \/ (H)=0) /\ (((pfen_plen_normalized_associate_result_backward)=0)))) \/ (((~((pfen_qlen_normalized_associate_result_backward)=0)) /\ (((~((H)=0)) /\ (((pfen_qlen_normalized_associate_result_backward)+(H)=S (pfen_plen_normalized_associate_result_backward)))))))) /\ ((forall pfc_index_normalized_associate_result_backward_productcoefficients. (exists pfa_gap_normalized_associate_result_backward_productcoefficientsbound. pfa_gap_normalized_associate_result_backward_productcoefficientsbound + S (pfc_index_normalized_associate_result_backward_productcoefficients) = (pfen_plen_normalized_associate_result_backward)) -> exists pfc_value_normalized_associate_result_backward_productcoefficients. ((((exists ff_h_pfp_normalized_associate_result_backward_productcoefficientsentry. ff_h_pfp_normalized_associate_result_backward_productcoefficientsentry + S (pfc_value_normalized_associate_result_backward_productcoefficients) = S ((S (pfc_index_normalized_associate_result_backward_productcoefficients)) * pfen_pc_normalized_associate_result_backward)) /\ exists ff_q_pfp_normalized_associate_result_backward_productcoefficientsentry. pfen_pb_normalized_associate_result_backward = ff_q_pfp_normalized_associate_result_backward_productcoefficientsentry * S ((S (pfc_index_normalized_associate_result_backward_productcoefficients)) * pfen_pc_normalized_associate_result_backward) + (pfc_value_normalized_associate_result_backward_productcoefficients))) /\ ((exists pfc_terms_code_normalized_associate_result_backward_productcoefficientscoefficient pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient pfc_natural_sum_normalized_associate_result_backward_productcoefficientscoefficient. ((forall pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonalbound. pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_associate_result_backward_productcoefficients))) -> exists pfc_value_normalized_associate_result_backward_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_associate_result_backward_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_associate_result_backward_productcoefficientscoefficient = ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient) + (pfc_value_normalized_associate_result_backward_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)+pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm=(pfc_index_normalized_associate_result_backward_productcoefficients)) /\ ((((((exists pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal) = (pfen_qlen_normalized_associate_result_backward)) /\ ((((exists ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalized_associate_result_backward)) /\ exists ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftentry. pfen_qb_normalized_associate_result_backward = ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalized_associate_result_backward) + (pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermleftoutside+(pfen_qlen_normalized_associate_result_backward)=(pfc_index_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm) = (H)) /\ ((((exists ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)) * hc)) /\ exists ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightentry. hb = ff_q_pfp_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)) * hc) + (pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_associate_result_backward_productcoefficientscoefficientdiagonaltermrightoutside+(H)=(pfc_complement_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_associate_result_backward_productcoefficientscoefficientdiagonal)=pfc_left_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm*pfc_right_normalized_associate_result_backward_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_associate_result_backward_productcoefficientscoefficient) = S ((S (S (pfc_index_normalized_associate_result_backward_productcoefficients))) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_associate_result_backward_productcoefficients))) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum) + (pfc_natural_sum_normalized_associate_result_backward_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_associate_result_backward_productcoefficients)) -> exists fs_a_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_associate_result_backward_productcoefficientscoefficient = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_associate_result_backward_productcoefficientscoefficient) + (fs_a_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum) + (fs_r_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum = fs_q_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum) + (fs_s_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_associate_result_backward_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientresiduebound. pfa_gap_normalized_associate_result_backward_productcoefficientscoefficientresiduebound + S (pfc_value_normalized_associate_result_backward_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_associate_result_backward_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_associate_result_backward_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_associate_result_backward_productcoefficientscoefficient) + (p) * pfa_offset_left_normalized_associate_result_backward_productcoefficientscoefficientresiduecongruence = (pfc_value_normalized_associate_result_backward_productcoefficients) + (p) * pfa_offset_right_normalized_associate_result_backward_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalized_associate_result_backward_target pfrep_left_normalized_associate_result_backward_target pfrep_right_normalized_associate_result_backward_target. ((exists pfrep_position_normalized_associate_result_backward_targetfirst. ((pfrep_position_normalized_associate_result_backward_targetfirst+S (pfrep_power_normalized_associate_result_backward_target)=(pfen_plen_normalized_associate_result_backward)) /\ ((((exists ff_h_pfp_normalized_associate_result_backward_targetfirstentry. ff_h_pfp_normalized_associate_result_backward_targetfirstentry + S (pfrep_left_normalized_associate_result_backward_target) = S ((S (pfrep_position_normalized_associate_result_backward_targetfirst)) * pfen_pc_normalized_associate_result_backward)) /\ exists ff_q_pfp_normalized_associate_result_backward_targetfirstentry. pfen_pb_normalized_associate_result_backward = ff_q_pfp_normalized_associate_result_backward_targetfirstentry * S ((S (pfrep_position_normalized_associate_result_backward_targetfirst)) * pfen_pc_normalized_associate_result_backward) + (pfrep_left_normalized_associate_result_backward_target)))))) \/ (((exists pfrep_gap_normalized_associate_result_backward_targetfirstoutside. pfrep_gap_normalized_associate_result_backward_targetfirstoutside+(pfen_plen_normalized_associate_result_backward)=(pfrep_power_normalized_associate_result_backward_target)) /\ (((pfrep_left_normalized_associate_result_backward_target)=0))))) -> ((exists pfrep_position_normalized_associate_result_backward_targetsecond. ((pfrep_position_normalized_associate_result_backward_targetsecond+S (pfrep_power_normalized_associate_result_backward_target)=(L)) /\ ((((exists ff_h_pfp_normalized_associate_result_backward_targetsecondentry. ff_h_pfp_normalized_associate_result_backward_targetsecondentry + S (pfrep_right_normalized_associate_result_backward_target) = S ((S (pfrep_position_normalized_associate_result_backward_targetsecond)) * ac)) /\ exists ff_q_pfp_normalized_associate_result_backward_targetsecondentry. ab = ff_q_pfp_normalized_associate_result_backward_targetsecondentry * S ((S (pfrep_position_normalized_associate_result_backward_targetsecond)) * ac) + (pfrep_right_normalized_associate_result_backward_target)))))) \/ (((exists pfrep_gap_normalized_associate_result_backward_targetsecondoutside. pfrep_gap_normalized_associate_result_backward_targetsecondoutside+(L)=(pfrep_power_normalized_associate_result_backward_target)) /\ (((pfrep_right_normalized_associate_result_backward_target)=0))))) -> pfrep_left_normalized_associate_result_backward_target=pfrep_right_normalized_associate_result_backward_target))))))))))))