prime_field_polynomial_monic_normalization_right_associates

forall p k gb gc hb hc L. (~((p) = 1) /\ forall pfa_factor_left_normalization_associates_prime pfa_factor_right_normalization_associates_prime. (p) = pfa_factor_left_normalization_associates_prime * pfa_factor_right_normalization_associates_prime -> pfa_factor_left_normalization_associates_prime = 1 \/ pfa_factor_right_normalization_associates_prime = 1) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_associates_actual. ((((exists ff_h_pfp_normalization_associates_actualsource. ff_h_pfp_normalization_associates_actualsource + S (pfm_leading_normalization_associates_actual) = S ((S (0)) * gc)) /\ exists ff_q_pfp_normalization_associates_actualsource. gb = ff_q_pfp_normalization_associates_actualsource * S ((S (0)) * gc) + (pfm_leading_normalization_associates_actual))) /\ ((((~((pfm_leading_normalization_associates_actual) = 0)) /\ ((((exists pfa_gap_normalization_associates_actualinversemultiplicationleft. pfa_gap_normalization_associates_actualinversemultiplicationleft + S (pfm_leading_normalization_associates_actual) = (p)) /\ (((exists pfa_gap_normalization_associates_actualinversemultiplicationright. pfa_gap_normalization_associates_actualinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_associates_actualinversemultiplicationresultbound. pfa_gap_normalization_associates_actualinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_associates_actualinversemultiplicationresultcongruence pfa_offset_right_normalization_associates_actualinversemultiplicationresultcongruence. ((pfm_leading_normalization_associates_actual) * (k)) + (p) * pfa_offset_left_normalization_associates_actualinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_associates_actualinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_associates_actualscalescalar. pfa_gap_normalization_associates_actualscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_associates_actualscale. (exists pfa_gap_normalization_associates_actualscaleindex. pfa_gap_normalization_associates_actualscaleindex + S (pfp_index_normalization_associates_actualscale) = (L)) -> exists pfp_source_normalization_associates_actualscale pfp_value_normalization_associates_actualscale. ((((exists ff_h_pfp_normalization_associates_actualscalesource. ff_h_pfp_normalization_associates_actualscalesource + S (pfp_source_normalization_associates_actualscale) = S ((S (pfp_index_normalization_associates_actualscale)) * gc)) /\ exists ff_q_pfp_normalization_associates_actualscalesource. gb = ff_q_pfp_normalization_associates_actualscalesource * S ((S (pfp_index_normalization_associates_actualscale)) * gc) + (pfp_source_normalization_associates_actualscale))) /\ (((((exists ff_h_pfp_normalization_associates_actualscaletarget. ff_h_pfp_normalization_associates_actualscaletarget + S (pfp_value_normalization_associates_actualscale) = S ((S (pfp_index_normalization_associates_actualscale)) * hc)) /\ exists ff_q_pfp_normalization_associates_actualscaletarget. hb = ff_q_pfp_normalization_associates_actualscaletarget * S ((S (pfp_index_normalization_associates_actualscale)) * hc) + (pfp_value_normalization_associates_actualscale))) /\ ((((exists pfa_gap_normalization_associates_actualscaleoperationleft. pfa_gap_normalization_associates_actualscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_associates_actualscaleoperationright. pfa_gap_normalization_associates_actualscaleoperationright + S (pfp_source_normalization_associates_actualscale) = (p)) /\ ((((exists pfa_gap_normalization_associates_actualscaleoperationresultbound. pfa_gap_normalization_associates_actualscaleoperationresultbound + S (pfp_value_normalization_associates_actualscale) = (p)) /\ ((exists pfa_offset_left_normalization_associates_actualscaleoperationresultcongruence pfa_offset_right_normalization_associates_actualscaleoperationresultcongruence. ((k) * (pfp_source_normalization_associates_actualscale)) + (p) * pfa_offset_left_normalization_associates_actualscaleoperationresultcongruence = (pfp_value_normalization_associates_actualscale) + (p) * pfa_offset_right_normalization_associates_actualscaleoperationresultcongruence)))))))))))))))))))))) -> (((((forall fom_index_pfp_normalization_associates_forward_canonical. (exists fom_gap_pfp_normalization_associates_forward_canonical_index_bound. fom_gap_pfp_normalization_associates_forward_canonical_index_bound + S (fom_index_pfp_normalization_associates_forward_canonical) = L) -> exists fom_value_pfp_normalization_associates_forward_canonical. ((((exists fom_beta_height_pfp_normalization_associates_forward_canonical_entry. fom_beta_height_pfp_normalization_associates_forward_canonical_entry + S (fom_value_pfp_normalization_associates_forward_canonical) = S ((S (fom_index_pfp_normalization_associates_forward_canonical)) * hc)) /\ exists fom_beta_quotient_pfp_normalization_associates_forward_canonical_entry. hb = fom_beta_quotient_pfp_normalization_associates_forward_canonical_entry * S ((S (fom_index_pfp_normalization_associates_forward_canonical)) * hc) + (fom_value_pfp_normalization_associates_forward_canonical))) /\ (exists fom_gap_pfp_normalization_associates_forward_canonical_value_bound. fom_gap_pfp_normalization_associates_forward_canonical_value_bound + S (fom_value_pfp_normalization_associates_forward_canonical) = p))) /\ ((exists pfen_qb_normalization_associates_forward pfen_qc_normalization_associates_forward pfen_qlen_normalization_associates_forward pfen_pb_normalization_associates_forward pfen_pc_normalization_associates_forward pfen_plen_normalization_associates_forward. ((((forall fom_index_pfp_normalization_associates_forward_productleft. (exists fom_gap_pfp_normalization_associates_forward_productleft_index_bound. fom_gap_pfp_normalization_associates_forward_productleft_index_bound + S (fom_index_pfp_normalization_associates_forward_productleft) = pfen_qlen_normalization_associates_forward) -> exists fom_value_pfp_normalization_associates_forward_productleft. ((((exists fom_beta_height_pfp_normalization_associates_forward_productleft_entry. fom_beta_height_pfp_normalization_associates_forward_productleft_entry + S (fom_value_pfp_normalization_associates_forward_productleft) = S ((S (fom_index_pfp_normalization_associates_forward_productleft)) * pfen_qc_normalization_associates_forward)) /\ exists fom_beta_quotient_pfp_normalization_associates_forward_productleft_entry. pfen_qb_normalization_associates_forward = fom_beta_quotient_pfp_normalization_associates_forward_productleft_entry * S ((S (fom_index_pfp_normalization_associates_forward_productleft)) * pfen_qc_normalization_associates_forward) + (fom_value_pfp_normalization_associates_forward_productleft))) /\ (exists fom_gap_pfp_normalization_associates_forward_productleft_value_bound. fom_gap_pfp_normalization_associates_forward_productleft_value_bound + S (fom_value_pfp_normalization_associates_forward_productleft) = p))) /\ (((forall fom_index_pfp_normalization_associates_forward_productright. (exists fom_gap_pfp_normalization_associates_forward_productright_index_bound. fom_gap_pfp_normalization_associates_forward_productright_index_bound + S (fom_index_pfp_normalization_associates_forward_productright) = L) -> exists fom_value_pfp_normalization_associates_forward_productright. ((((exists fom_beta_height_pfp_normalization_associates_forward_productright_entry. fom_beta_height_pfp_normalization_associates_forward_productright_entry + S (fom_value_pfp_normalization_associates_forward_productright) = S ((S (fom_index_pfp_normalization_associates_forward_productright)) * gc)) /\ exists fom_beta_quotient_pfp_normalization_associates_forward_productright_entry. gb = fom_beta_quotient_pfp_normalization_associates_forward_productright_entry * S ((S (fom_index_pfp_normalization_associates_forward_productright)) * gc) + (fom_value_pfp_normalization_associates_forward_productright))) /\ (exists fom_gap_pfp_normalization_associates_forward_productright_value_bound. fom_gap_pfp_normalization_associates_forward_productright_value_bound + S (fom_value_pfp_normalization_associates_forward_productright) = p))) /\ (((((((pfen_qlen_normalization_associates_forward)=0 \/ (L)=0) /\ (((pfen_plen_normalization_associates_forward)=0)))) \/ (((~((pfen_qlen_normalization_associates_forward)=0)) /\ (((~((L)=0)) /\ (((pfen_qlen_normalization_associates_forward)+(L)=S (pfen_plen_normalization_associates_forward)))))))) /\ ((forall pfc_index_normalization_associates_forward_productcoefficients. (exists pfa_gap_normalization_associates_forward_productcoefficientsbound. pfa_gap_normalization_associates_forward_productcoefficientsbound + S (pfc_index_normalization_associates_forward_productcoefficients) = (pfen_plen_normalization_associates_forward)) -> exists pfc_value_normalization_associates_forward_productcoefficients. ((((exists ff_h_pfp_normalization_associates_forward_productcoefficientsentry. ff_h_pfp_normalization_associates_forward_productcoefficientsentry + S (pfc_value_normalization_associates_forward_productcoefficients) = S ((S (pfc_index_normalization_associates_forward_productcoefficients)) * pfen_pc_normalization_associates_forward)) /\ exists ff_q_pfp_normalization_associates_forward_productcoefficientsentry. pfen_pb_normalization_associates_forward = ff_q_pfp_normalization_associates_forward_productcoefficientsentry * S ((S (pfc_index_normalization_associates_forward_productcoefficients)) * pfen_pc_normalization_associates_forward) + (pfc_value_normalization_associates_forward_productcoefficients))) /\ ((exists pfc_terms_code_normalization_associates_forward_productcoefficientscoefficient pfc_terms_scale_normalization_associates_forward_productcoefficientscoefficient pfc_natural_sum_normalization_associates_forward_productcoefficientscoefficient. ((forall pfc_index_normalization_associates_forward_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalization_associates_forward_productcoefficientscoefficientdiagonalbound. pfa_gap_normalization_associates_forward_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalization_associates_forward_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalization_associates_forward_productcoefficients))) -> exists pfc_value_normalization_associates_forward_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalization_associates_forward_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalization_associates_forward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalization_associates_forward_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalization_associates_forward_productcoefficientscoefficient = ff_q_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalization_associates_forward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalization_associates_forward_productcoefficientscoefficient) + (pfc_value_normalization_associates_forward_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalization_associates_forward_productcoefficientscoefficientdiagonalterm pfc_left_normalization_associates_forward_productcoefficientscoefficientdiagonalterm pfc_right_normalization_associates_forward_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalization_associates_forward_productcoefficientscoefficientdiagonal)+pfc_complement_normalization_associates_forward_productcoefficientscoefficientdiagonalterm=(pfc_index_normalization_associates_forward_productcoefficients)) /\ ((((((exists pfa_gap_normalization_associates_forward_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalization_associates_forward_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalization_associates_forward_productcoefficientscoefficientdiagonal) = (pfen_qlen_normalization_associates_forward)) /\ ((((exists ff_h_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalization_associates_forward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalization_associates_forward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalization_associates_forward)) /\ exists ff_q_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonaltermleftentry. pfen_qb_normalization_associates_forward = ff_q_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalization_associates_forward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalization_associates_forward) + (pfc_left_normalization_associates_forward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_associates_forward_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalization_associates_forward_productcoefficientscoefficientdiagonaltermleftoutside+(pfen_qlen_normalization_associates_forward)=(pfc_index_normalization_associates_forward_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalization_associates_forward_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalization_associates_forward_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalization_associates_forward_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalization_associates_forward_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalization_associates_forward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalization_associates_forward_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_normalization_associates_forward_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalization_associates_forward_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_normalization_associates_forward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_associates_forward_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalization_associates_forward_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_normalization_associates_forward_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalization_associates_forward_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalization_associates_forward_productcoefficientscoefficientdiagonal)=pfc_left_normalization_associates_forward_productcoefficientscoefficientdiagonalterm*pfc_right_normalization_associates_forward_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalization_associates_forward_productcoefficientscoefficientsum fs_v_pfc_normalization_associates_forward_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalization_associates_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalization_associates_forward_productcoefficientscoefficientsum = fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalization_associates_forward_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalization_associates_forward_productcoefficientscoefficient) = S ((S (S (pfc_index_normalization_associates_forward_productcoefficients))) * fs_v_pfc_normalization_associates_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalization_associates_forward_productcoefficientscoefficientsum = fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalization_associates_forward_productcoefficients))) * fs_v_pfc_normalization_associates_forward_productcoefficientscoefficientsum) + (pfc_natural_sum_normalization_associates_forward_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalization_associates_forward_productcoefficients)) -> exists fs_a_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalization_associates_forward_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalization_associates_forward_productcoefficientscoefficient = fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalization_associates_forward_productcoefficientscoefficient) + (fs_a_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_associates_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalization_associates_forward_productcoefficientscoefficientsum = fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_associates_forward_productcoefficientscoefficientsum) + (fs_r_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_associates_forward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalization_associates_forward_productcoefficientscoefficientsum = fs_q_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_associates_forward_productcoefficientscoefficientsum) + (fs_s_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalization_associates_forward_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalization_associates_forward_productcoefficientscoefficientresiduebound. pfa_gap_normalization_associates_forward_productcoefficientscoefficientresiduebound + S (pfc_value_normalization_associates_forward_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalization_associates_forward_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalization_associates_forward_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalization_associates_forward_productcoefficientscoefficient) + (p) * pfa_offset_left_normalization_associates_forward_productcoefficientscoefficientresiduecongruence = (pfc_value_normalization_associates_forward_productcoefficients) + (p) * pfa_offset_right_normalization_associates_forward_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalization_associates_forward_target pfrep_left_normalization_associates_forward_target pfrep_right_normalization_associates_forward_target. ((exists pfrep_position_normalization_associates_forward_targetfirst. ((pfrep_position_normalization_associates_forward_targetfirst+S (pfrep_power_normalization_associates_forward_target)=(pfen_plen_normalization_associates_forward)) /\ ((((exists ff_h_pfp_normalization_associates_forward_targetfirstentry. ff_h_pfp_normalization_associates_forward_targetfirstentry + S (pfrep_left_normalization_associates_forward_target) = S ((S (pfrep_position_normalization_associates_forward_targetfirst)) * pfen_pc_normalization_associates_forward)) /\ exists ff_q_pfp_normalization_associates_forward_targetfirstentry. pfen_pb_normalization_associates_forward = ff_q_pfp_normalization_associates_forward_targetfirstentry * S ((S (pfrep_position_normalization_associates_forward_targetfirst)) * pfen_pc_normalization_associates_forward) + (pfrep_left_normalization_associates_forward_target)))))) \/ (((exists pfrep_gap_normalization_associates_forward_targetfirstoutside. pfrep_gap_normalization_associates_forward_targetfirstoutside+(pfen_plen_normalization_associates_forward)=(pfrep_power_normalization_associates_forward_target)) /\ (((pfrep_left_normalization_associates_forward_target)=0))))) -> ((exists pfrep_position_normalization_associates_forward_targetsecond. ((pfrep_position_normalization_associates_forward_targetsecond+S (pfrep_power_normalization_associates_forward_target)=(L)) /\ ((((exists ff_h_pfp_normalization_associates_forward_targetsecondentry. ff_h_pfp_normalization_associates_forward_targetsecondentry + S (pfrep_right_normalization_associates_forward_target) = S ((S (pfrep_position_normalization_associates_forward_targetsecond)) * hc)) /\ exists ff_q_pfp_normalization_associates_forward_targetsecondentry. hb = ff_q_pfp_normalization_associates_forward_targetsecondentry * S ((S (pfrep_position_normalization_associates_forward_targetsecond)) * hc) + (pfrep_right_normalization_associates_forward_target)))))) \/ (((exists pfrep_gap_normalization_associates_forward_targetsecondoutside. pfrep_gap_normalization_associates_forward_targetsecondoutside+(L)=(pfrep_power_normalization_associates_forward_target)) /\ (((pfrep_right_normalization_associates_forward_target)=0))))) -> pfrep_left_normalization_associates_forward_target=pfrep_right_normalization_associates_forward_target))))))) /\ ((((forall fom_index_pfp_normalization_associates_backward_canonical. (exists fom_gap_pfp_normalization_associates_backward_canonical_index_bound. fom_gap_pfp_normalization_associates_backward_canonical_index_bound + S (fom_index_pfp_normalization_associates_backward_canonical) = L) -> exists fom_value_pfp_normalization_associates_backward_canonical. ((((exists fom_beta_height_pfp_normalization_associates_backward_canonical_entry. fom_beta_height_pfp_normalization_associates_backward_canonical_entry + S (fom_value_pfp_normalization_associates_backward_canonical) = S ((S (fom_index_pfp_normalization_associates_backward_canonical)) * gc)) /\ exists fom_beta_quotient_pfp_normalization_associates_backward_canonical_entry. gb = fom_beta_quotient_pfp_normalization_associates_backward_canonical_entry * S ((S (fom_index_pfp_normalization_associates_backward_canonical)) * gc) + (fom_value_pfp_normalization_associates_backward_canonical))) /\ (exists fom_gap_pfp_normalization_associates_backward_canonical_value_bound. fom_gap_pfp_normalization_associates_backward_canonical_value_bound + S (fom_value_pfp_normalization_associates_backward_canonical) = p))) /\ ((exists pfen_qb_normalization_associates_backward pfen_qc_normalization_associates_backward pfen_qlen_normalization_associates_backward pfen_pb_normalization_associates_backward pfen_pc_normalization_associates_backward pfen_plen_normalization_associates_backward. ((((forall fom_index_pfp_normalization_associates_backward_productleft. (exists fom_gap_pfp_normalization_associates_backward_productleft_index_bound. fom_gap_pfp_normalization_associates_backward_productleft_index_bound + S (fom_index_pfp_normalization_associates_backward_productleft) = pfen_qlen_normalization_associates_backward) -> exists fom_value_pfp_normalization_associates_backward_productleft. ((((exists fom_beta_height_pfp_normalization_associates_backward_productleft_entry. fom_beta_height_pfp_normalization_associates_backward_productleft_entry + S (fom_value_pfp_normalization_associates_backward_productleft) = S ((S (fom_index_pfp_normalization_associates_backward_productleft)) * pfen_qc_normalization_associates_backward)) /\ exists fom_beta_quotient_pfp_normalization_associates_backward_productleft_entry. pfen_qb_normalization_associates_backward = fom_beta_quotient_pfp_normalization_associates_backward_productleft_entry * S ((S (fom_index_pfp_normalization_associates_backward_productleft)) * pfen_qc_normalization_associates_backward) + (fom_value_pfp_normalization_associates_backward_productleft))) /\ (exists fom_gap_pfp_normalization_associates_backward_productleft_value_bound. fom_gap_pfp_normalization_associates_backward_productleft_value_bound + S (fom_value_pfp_normalization_associates_backward_productleft) = p))) /\ (((forall fom_index_pfp_normalization_associates_backward_productright. (exists fom_gap_pfp_normalization_associates_backward_productright_index_bound. fom_gap_pfp_normalization_associates_backward_productright_index_bound + S (fom_index_pfp_normalization_associates_backward_productright) = L) -> exists fom_value_pfp_normalization_associates_backward_productright. ((((exists fom_beta_height_pfp_normalization_associates_backward_productright_entry. fom_beta_height_pfp_normalization_associates_backward_productright_entry + S (fom_value_pfp_normalization_associates_backward_productright) = S ((S (fom_index_pfp_normalization_associates_backward_productright)) * hc)) /\ exists fom_beta_quotient_pfp_normalization_associates_backward_productright_entry. hb = fom_beta_quotient_pfp_normalization_associates_backward_productright_entry * S ((S (fom_index_pfp_normalization_associates_backward_productright)) * hc) + (fom_value_pfp_normalization_associates_backward_productright))) /\ (exists fom_gap_pfp_normalization_associates_backward_productright_value_bound. fom_gap_pfp_normalization_associates_backward_productright_value_bound + S (fom_value_pfp_normalization_associates_backward_productright) = p))) /\ (((((((pfen_qlen_normalization_associates_backward)=0 \/ (L)=0) /\ (((pfen_plen_normalization_associates_backward)=0)))) \/ (((~((pfen_qlen_normalization_associates_backward)=0)) /\ (((~((L)=0)) /\ (((pfen_qlen_normalization_associates_backward)+(L)=S (pfen_plen_normalization_associates_backward)))))))) /\ ((forall pfc_index_normalization_associates_backward_productcoefficients. (exists pfa_gap_normalization_associates_backward_productcoefficientsbound. pfa_gap_normalization_associates_backward_productcoefficientsbound + S (pfc_index_normalization_associates_backward_productcoefficients) = (pfen_plen_normalization_associates_backward)) -> exists pfc_value_normalization_associates_backward_productcoefficients. ((((exists ff_h_pfp_normalization_associates_backward_productcoefficientsentry. ff_h_pfp_normalization_associates_backward_productcoefficientsentry + S (pfc_value_normalization_associates_backward_productcoefficients) = S ((S (pfc_index_normalization_associates_backward_productcoefficients)) * pfen_pc_normalization_associates_backward)) /\ exists ff_q_pfp_normalization_associates_backward_productcoefficientsentry. pfen_pb_normalization_associates_backward = ff_q_pfp_normalization_associates_backward_productcoefficientsentry * S ((S (pfc_index_normalization_associates_backward_productcoefficients)) * pfen_pc_normalization_associates_backward) + (pfc_value_normalization_associates_backward_productcoefficients))) /\ ((exists pfc_terms_code_normalization_associates_backward_productcoefficientscoefficient pfc_terms_scale_normalization_associates_backward_productcoefficientscoefficient pfc_natural_sum_normalization_associates_backward_productcoefficientscoefficient. ((forall pfc_index_normalization_associates_backward_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalization_associates_backward_productcoefficientscoefficientdiagonalbound. pfa_gap_normalization_associates_backward_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalization_associates_backward_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalization_associates_backward_productcoefficients))) -> exists pfc_value_normalization_associates_backward_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalization_associates_backward_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalization_associates_backward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalization_associates_backward_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalization_associates_backward_productcoefficientscoefficient = ff_q_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalization_associates_backward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalization_associates_backward_productcoefficientscoefficient) + (pfc_value_normalization_associates_backward_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalization_associates_backward_productcoefficientscoefficientdiagonalterm pfc_left_normalization_associates_backward_productcoefficientscoefficientdiagonalterm pfc_right_normalization_associates_backward_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalization_associates_backward_productcoefficientscoefficientdiagonal)+pfc_complement_normalization_associates_backward_productcoefficientscoefficientdiagonalterm=(pfc_index_normalization_associates_backward_productcoefficients)) /\ ((((((exists pfa_gap_normalization_associates_backward_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalization_associates_backward_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalization_associates_backward_productcoefficientscoefficientdiagonal) = (pfen_qlen_normalization_associates_backward)) /\ ((((exists ff_h_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalization_associates_backward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalization_associates_backward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalization_associates_backward)) /\ exists ff_q_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonaltermleftentry. pfen_qb_normalization_associates_backward = ff_q_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalization_associates_backward_productcoefficientscoefficientdiagonal)) * pfen_qc_normalization_associates_backward) + (pfc_left_normalization_associates_backward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_associates_backward_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalization_associates_backward_productcoefficientscoefficientdiagonaltermleftoutside+(pfen_qlen_normalization_associates_backward)=(pfc_index_normalization_associates_backward_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalization_associates_backward_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalization_associates_backward_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalization_associates_backward_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalization_associates_backward_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalization_associates_backward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalization_associates_backward_productcoefficientscoefficientdiagonalterm)) * hc)) /\ exists ff_q_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonaltermrightentry. hb = ff_q_pfp_normalization_associates_backward_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalization_associates_backward_productcoefficientscoefficientdiagonalterm)) * hc) + (pfc_right_normalization_associates_backward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalization_associates_backward_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalization_associates_backward_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_normalization_associates_backward_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalization_associates_backward_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalization_associates_backward_productcoefficientscoefficientdiagonal)=pfc_left_normalization_associates_backward_productcoefficientscoefficientdiagonalterm*pfc_right_normalization_associates_backward_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalization_associates_backward_productcoefficientscoefficientsum fs_v_pfc_normalization_associates_backward_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalization_associates_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalization_associates_backward_productcoefficientscoefficientsum = fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalization_associates_backward_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalization_associates_backward_productcoefficientscoefficient) = S ((S (S (pfc_index_normalization_associates_backward_productcoefficients))) * fs_v_pfc_normalization_associates_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalization_associates_backward_productcoefficientscoefficientsum = fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalization_associates_backward_productcoefficients))) * fs_v_pfc_normalization_associates_backward_productcoefficientscoefficientsum) + (pfc_natural_sum_normalization_associates_backward_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalization_associates_backward_productcoefficients)) -> exists fs_a_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalization_associates_backward_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalization_associates_backward_productcoefficientscoefficient = fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalization_associates_backward_productcoefficientscoefficient) + (fs_a_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_associates_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalization_associates_backward_productcoefficientscoefficientsum = fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_associates_backward_productcoefficientscoefficientsum) + (fs_r_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_associates_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalization_associates_backward_productcoefficientscoefficientsum = fs_q_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalization_associates_backward_productcoefficientscoefficientsum) + (fs_s_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalization_associates_backward_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalization_associates_backward_productcoefficientscoefficientresiduebound. pfa_gap_normalization_associates_backward_productcoefficientscoefficientresiduebound + S (pfc_value_normalization_associates_backward_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalization_associates_backward_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalization_associates_backward_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalization_associates_backward_productcoefficientscoefficient) + (p) * pfa_offset_left_normalization_associates_backward_productcoefficientscoefficientresiduecongruence = (pfc_value_normalization_associates_backward_productcoefficients) + (p) * pfa_offset_right_normalization_associates_backward_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalization_associates_backward_target pfrep_left_normalization_associates_backward_target pfrep_right_normalization_associates_backward_target. ((exists pfrep_position_normalization_associates_backward_targetfirst. ((pfrep_position_normalization_associates_backward_targetfirst+S (pfrep_power_normalization_associates_backward_target)=(pfen_plen_normalization_associates_backward)) /\ ((((exists ff_h_pfp_normalization_associates_backward_targetfirstentry. ff_h_pfp_normalization_associates_backward_targetfirstentry + S (pfrep_left_normalization_associates_backward_target) = S ((S (pfrep_position_normalization_associates_backward_targetfirst)) * pfen_pc_normalization_associates_backward)) /\ exists ff_q_pfp_normalization_associates_backward_targetfirstentry. pfen_pb_normalization_associates_backward = ff_q_pfp_normalization_associates_backward_targetfirstentry * S ((S (pfrep_position_normalization_associates_backward_targetfirst)) * pfen_pc_normalization_associates_backward) + (pfrep_left_normalization_associates_backward_target)))))) \/ (((exists pfrep_gap_normalization_associates_backward_targetfirstoutside. pfrep_gap_normalization_associates_backward_targetfirstoutside+(pfen_plen_normalization_associates_backward)=(pfrep_power_normalization_associates_backward_target)) /\ (((pfrep_left_normalization_associates_backward_target)=0))))) -> ((exists pfrep_position_normalization_associates_backward_targetsecond. ((pfrep_position_normalization_associates_backward_targetsecond+S (pfrep_power_normalization_associates_backward_target)=(L)) /\ ((((exists ff_h_pfp_normalization_associates_backward_targetsecondentry. ff_h_pfp_normalization_associates_backward_targetsecondentry + S (pfrep_right_normalization_associates_backward_target) = S ((S (pfrep_position_normalization_associates_backward_targetsecond)) * gc)) /\ exists ff_q_pfp_normalization_associates_backward_targetsecondentry. gb = ff_q_pfp_normalization_associates_backward_targetsecondentry * S ((S (pfrep_position_normalization_associates_backward_targetsecond)) * gc) + (pfrep_right_normalization_associates_backward_target)))))) \/ (((exists pfrep_gap_normalization_associates_backward_targetsecondoutside. pfrep_gap_normalization_associates_backward_targetsecondoutside+(L)=(pfrep_power_normalization_associates_backward_target)) /\ (((pfrep_right_normalization_associates_backward_target)=0))))) -> pfrep_left_normalization_associates_backward_target=pfrep_right_normalization_associates_backward_target))))))))))