Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall p ab ac L bb bc M pb pc N cb cc J q0b q0c K0 r0b r0c U0 s0b s0c V0 c db dc q1b q1c K1 r1b r1c U1 s1b s1c V1. (~((p) = 1) /\ forall pfa_factor_left_append_step_prime pfa_factor_right_append_step_prime. (p) = pfa_factor_left_append_step_prime * pfa_factor_right_append_step_prime -> pfa_factor_left_append_step_prime = 1 \/ pfa_factor_right_append_step_prime = 1) -> (((forall fom_index_pfp_append_step_ABleft. (exists fom_gap_pfp_append_step_ABleft_index_bound. fom_gap_pfp_append_step_ABleft_index_bound + S (fom_index_pfp_append_step_ABleft) = L) -> exists fom_value_pfp_append_step_ABleft. ((((exists fom_beta_height_pfp_append_step_ABleft_entry. fom_beta_height_pfp_append_step_ABleft_entry + S (fom_value_pfp_append_step_ABleft) = S ((S (fom_index_pfp_append_step_ABleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_step_ABleft_entry. ab = fom_beta_quotient_pfp_append_step_ABleft_entry * S ((S (fom_index_pfp_append_step_ABleft)) * ac) + (fom_value_pfp_append_step_ABleft))) /\ (exists fom_gap_pfp_append_step_ABleft_value_bound. fom_gap_pfp_append_step_ABleft_value_bound + S (fom_value_pfp_append_step_ABleft) = p))) /\ (((forall fom_index_pfp_append_step_ABright. (exists fom_gap_pfp_append_step_ABright_index_bound. fom_gap_pfp_append_step_ABright_index_bound + S (fom_index_pfp_append_step_ABright) = M) -> exists fom_value_pfp_append_step_ABright. ((((exists fom_beta_height_pfp_append_step_ABright_entry. fom_beta_height_pfp_append_step_ABright_entry + S (fom_value_pfp_append_step_ABright) = S ((S (fom_index_pfp_append_step_ABright)) * bc)) /\ exists fom_beta_quotient_pfp_append_step_ABright_entry. bb = fom_beta_quotient_pfp_append_step_ABright_entry * S ((S (fom_index_pfp_append_step_ABright)) * bc) + (fom_value_pfp_append_step_ABright))) /\ (exists fom_gap_pfp_append_step_ABright_value_bound. fom_gap_pfp_append_step_ABright_value_bound + S (fom_value_pfp_append_step_ABright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_append_step_ABcoefficients. (exists pfa_gap_append_step_ABcoefficientsbound. pfa_gap_append_step_ABcoefficientsbound + S (pfc_index_append_step_ABcoefficients) = (N)) -> exists pfc_value_append_step_ABcoefficients. ((((exists ff_h_pfp_append_step_ABcoefficientsentry. ff_h_pfp_append_step_ABcoefficientsentry + S (pfc_value_append_step_ABcoefficients) = S ((S (pfc_index_append_step_ABcoefficients)) * pc)) /\ exists ff_q_pfp_append_step_ABcoefficientsentry. pb = ff_q_pfp_append_step_ABcoefficientsentry * S ((S (pfc_index_append_step_ABcoefficients)) * pc) + (pfc_value_append_step_ABcoefficients))) /\ ((exists pfc_terms_code_append_step_ABcoefficientscoefficient pfc_terms_scale_append_step_ABcoefficientscoefficient pfc_natural_sum_append_step_ABcoefficientscoefficient. ((forall pfc_index_append_step_ABcoefficientscoefficientdiagonal. (exists pfa_gap_append_step_ABcoefficientscoefficientdiagonalbound. pfa_gap_append_step_ABcoefficientscoefficientdiagonalbound + S (pfc_index_append_step_ABcoefficientscoefficientdiagonal) = (S (pfc_index_append_step_ABcoefficients))) -> exists pfc_value_append_step_ABcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_ABcoefficientscoefficientdiagonalentry. ff_h_pfp_append_step_ABcoefficientscoefficientdiagonalentry + S (pfc_value_append_step_ABcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_ABcoefficientscoefficient)) /\ exists ff_q_pfp_append_step_ABcoefficientscoefficientdiagonalentry. pfc_terms_code_append_step_ABcoefficientscoefficient = ff_q_pfp_append_step_ABcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_ABcoefficientscoefficient) + (pfc_value_append_step_ABcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm pfc_left_append_step_ABcoefficientscoefficientdiagonalterm pfc_right_append_step_ABcoefficientscoefficientdiagonalterm. (((pfc_index_append_step_ABcoefficientscoefficientdiagonal)+pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm=(pfc_index_append_step_ABcoefficients)) /\ ((((((exists pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_ABcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_step_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_step_ABcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_ABcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_append_step_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_ABcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_ABcoefficientscoefficientdiagonal)=pfc_left_append_step_ABcoefficientscoefficientdiagonalterm*pfc_right_append_step_ABcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_ABcoefficientscoefficientsum fs_v_pfc_append_step_ABcoefficientscoefficientsum. ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_start. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_start. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_ABcoefficientscoefficient) = S ((S (S (pfc_index_append_step_ABcoefficients))) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_ABcoefficients))) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (pfc_natural_sum_append_step_ABcoefficientscoefficient))) /\ forall fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_ABcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_ABcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps = S (pfc_index_append_step_ABcoefficients)) -> exists fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_ABcoefficientscoefficient)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_ABcoefficientscoefficient = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_ABcoefficientscoefficient) + (fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps = fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps + fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_ABcoefficientscoefficientresiduebound. pfa_gap_append_step_ABcoefficientscoefficientresiduebound + S (pfc_value_append_step_ABcoefficients) = (p)) /\ ((exists pfa_offset_left_append_step_ABcoefficientscoefficientresiduecongruence pfa_offset_right_append_step_ABcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_ABcoefficientscoefficient) + (p) * pfa_offset_left_append_step_ABcoefficientscoefficientresiduecongruence = (pfc_value_append_step_ABcoefficients) + (p) * pfa_offset_right_append_step_ABcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_Q0left. (exists fom_gap_pfp_append_step_Q0left_index_bound. fom_gap_pfp_append_step_Q0left_index_bound + S (fom_index_pfp_append_step_Q0left) = M) -> exists fom_value_pfp_append_step_Q0left. ((((exists fom_beta_height_pfp_append_step_Q0left_entry. fom_beta_height_pfp_append_step_Q0left_entry + S (fom_value_pfp_append_step_Q0left) = S ((S (fom_index_pfp_append_step_Q0left)) * bc)) /\ exists fom_beta_quotient_pfp_append_step_Q0left_entry. bb = fom_beta_quotient_pfp_append_step_Q0left_entry * S ((S (fom_index_pfp_append_step_Q0left)) * bc) + (fom_value_pfp_append_step_Q0left))) /\ (exists fom_gap_pfp_append_step_Q0left_value_bound. fom_gap_pfp_append_step_Q0left_value_bound + S (fom_value_pfp_append_step_Q0left) = p))) /\ (((forall fom_index_pfp_append_step_Q0right. (exists fom_gap_pfp_append_step_Q0right_index_bound. fom_gap_pfp_append_step_Q0right_index_bound + S (fom_index_pfp_append_step_Q0right) = J) -> exists fom_value_pfp_append_step_Q0right. ((((exists fom_beta_height_pfp_append_step_Q0right_entry. fom_beta_height_pfp_append_step_Q0right_entry + S (fom_value_pfp_append_step_Q0right) = S ((S (fom_index_pfp_append_step_Q0right)) * cc)) /\ exists fom_beta_quotient_pfp_append_step_Q0right_entry. cb = fom_beta_quotient_pfp_append_step_Q0right_entry * S ((S (fom_index_pfp_append_step_Q0right)) * cc) + (fom_value_pfp_append_step_Q0right))) /\ (exists fom_gap_pfp_append_step_Q0right_value_bound. fom_gap_pfp_append_step_Q0right_value_bound + S (fom_value_pfp_append_step_Q0right) = p))) /\ (((((((M)=0 \/ (J)=0) /\ (((K0)=0)))) \/ (((~((M)=0)) /\ (((~((J)=0)) /\ (((M)+(J)=S (K0)))))))) /\ ((forall pfc_index_append_step_Q0coefficients. (exists pfa_gap_append_step_Q0coefficientsbound. pfa_gap_append_step_Q0coefficientsbound + S (pfc_index_append_step_Q0coefficients) = (K0)) -> exists pfc_value_append_step_Q0coefficients. ((((exists ff_h_pfp_append_step_Q0coefficientsentry. ff_h_pfp_append_step_Q0coefficientsentry + S (pfc_value_append_step_Q0coefficients) = S ((S (pfc_index_append_step_Q0coefficients)) * q0c)) /\ exists ff_q_pfp_append_step_Q0coefficientsentry. q0b = ff_q_pfp_append_step_Q0coefficientsentry * S ((S (pfc_index_append_step_Q0coefficients)) * q0c) + (pfc_value_append_step_Q0coefficients))) /\ ((exists pfc_terms_code_append_step_Q0coefficientscoefficient pfc_terms_scale_append_step_Q0coefficientscoefficient pfc_natural_sum_append_step_Q0coefficientscoefficient. ((forall pfc_index_append_step_Q0coefficientscoefficientdiagonal. (exists pfa_gap_append_step_Q0coefficientscoefficientdiagonalbound. pfa_gap_append_step_Q0coefficientscoefficientdiagonalbound + S (pfc_index_append_step_Q0coefficientscoefficientdiagonal) = (S (pfc_index_append_step_Q0coefficients))) -> exists pfc_value_append_step_Q0coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_Q0coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_Q0coefficientscoefficientdiagonalentry + S (pfc_value_append_step_Q0coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_Q0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q0coefficientscoefficient)) /\ exists ff_q_pfp_append_step_Q0coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_Q0coefficientscoefficient = ff_q_pfp_append_step_Q0coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_Q0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q0coefficientscoefficient) + (pfc_value_append_step_Q0coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm pfc_left_append_step_Q0coefficientscoefficientdiagonalterm pfc_right_append_step_Q0coefficientscoefficientdiagonalterm. (((pfc_index_append_step_Q0coefficientscoefficientdiagonal)+pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm=(pfc_index_append_step_Q0coefficients)) /\ ((((((exists pfa_gap_append_step_Q0coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_Q0coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_Q0coefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_append_step_Q0coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_Q0coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_Q0coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_Q0coefficientscoefficientdiagonal)) * bc)) /\ exists ff_q_pfp_append_step_Q0coefficientscoefficientdiagonaltermleftentry. bb = ff_q_pfp_append_step_Q0coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_Q0coefficientscoefficientdiagonal)) * bc) + (pfc_left_append_step_Q0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q0coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_Q0coefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_append_step_Q0coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_Q0coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_Q0coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_Q0coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_append_step_Q0coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_Q0coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_Q0coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_append_step_Q0coefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_append_step_Q0coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm)) * cc) + (pfc_right_append_step_Q0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q0coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_Q0coefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_append_step_Q0coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_Q0coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_Q0coefficientscoefficientdiagonal)=pfc_left_append_step_Q0coefficientscoefficientdiagonalterm*pfc_right_append_step_Q0coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_Q0coefficientscoefficientsum fs_v_pfc_append_step_Q0coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_start. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_start. fs_u_pfc_append_step_Q0coefficientscoefficientsum = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_Q0coefficientscoefficient) = S ((S (S (pfc_index_append_step_Q0coefficients))) * fs_v_pfc_append_step_Q0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_Q0coefficientscoefficientsum = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_Q0coefficients))) * fs_v_pfc_append_step_Q0coefficientscoefficientsum) + (pfc_natural_sum_append_step_Q0coefficientscoefficient))) /\ forall fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_Q0coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_Q0coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps = S (pfc_index_append_step_Q0coefficients)) -> exists fs_a_pfc_append_step_Q0coefficientscoefficientsum_body_steps fs_r_pfc_append_step_Q0coefficientscoefficientsum_body_steps fs_s_pfc_append_step_Q0coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_Q0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q0coefficientscoefficient)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_Q0coefficientscoefficient = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q0coefficientscoefficient) + (fs_a_pfc_append_step_Q0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_Q0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_Q0coefficientscoefficientsum = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum) + (fs_r_pfc_append_step_Q0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_Q0coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_Q0coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_Q0coefficientscoefficientsum = fs_q_pfc_append_step_Q0coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_Q0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q0coefficientscoefficientsum) + (fs_s_pfc_append_step_Q0coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_Q0coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_Q0coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_Q0coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_Q0coefficientscoefficientresiduebound. pfa_gap_append_step_Q0coefficientscoefficientresiduebound + S (pfc_value_append_step_Q0coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_Q0coefficientscoefficientresiduecongruence pfa_offset_right_append_step_Q0coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_Q0coefficientscoefficient) + (p) * pfa_offset_left_append_step_Q0coefficientscoefficientresiduecongruence = (pfc_value_append_step_Q0coefficients) + (p) * pfa_offset_right_append_step_Q0coefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_R0left. (exists fom_gap_pfp_append_step_R0left_index_bound. fom_gap_pfp_append_step_R0left_index_bound + S (fom_index_pfp_append_step_R0left) = N) -> exists fom_value_pfp_append_step_R0left. ((((exists fom_beta_height_pfp_append_step_R0left_entry. fom_beta_height_pfp_append_step_R0left_entry + S (fom_value_pfp_append_step_R0left) = S ((S (fom_index_pfp_append_step_R0left)) * pc)) /\ exists fom_beta_quotient_pfp_append_step_R0left_entry. pb = fom_beta_quotient_pfp_append_step_R0left_entry * S ((S (fom_index_pfp_append_step_R0left)) * pc) + (fom_value_pfp_append_step_R0left))) /\ (exists fom_gap_pfp_append_step_R0left_value_bound. fom_gap_pfp_append_step_R0left_value_bound + S (fom_value_pfp_append_step_R0left) = p))) /\ (((forall fom_index_pfp_append_step_R0right. (exists fom_gap_pfp_append_step_R0right_index_bound. fom_gap_pfp_append_step_R0right_index_bound + S (fom_index_pfp_append_step_R0right) = J) -> exists fom_value_pfp_append_step_R0right. ((((exists fom_beta_height_pfp_append_step_R0right_entry. fom_beta_height_pfp_append_step_R0right_entry + S (fom_value_pfp_append_step_R0right) = S ((S (fom_index_pfp_append_step_R0right)) * cc)) /\ exists fom_beta_quotient_pfp_append_step_R0right_entry. cb = fom_beta_quotient_pfp_append_step_R0right_entry * S ((S (fom_index_pfp_append_step_R0right)) * cc) + (fom_value_pfp_append_step_R0right))) /\ (exists fom_gap_pfp_append_step_R0right_value_bound. fom_gap_pfp_append_step_R0right_value_bound + S (fom_value_pfp_append_step_R0right) = p))) /\ (((((((N)=0 \/ (J)=0) /\ (((U0)=0)))) \/ (((~((N)=0)) /\ (((~((J)=0)) /\ (((N)+(J)=S (U0)))))))) /\ ((forall pfc_index_append_step_R0coefficients. (exists pfa_gap_append_step_R0coefficientsbound. pfa_gap_append_step_R0coefficientsbound + S (pfc_index_append_step_R0coefficients) = (U0)) -> exists pfc_value_append_step_R0coefficients. ((((exists ff_h_pfp_append_step_R0coefficientsentry. ff_h_pfp_append_step_R0coefficientsentry + S (pfc_value_append_step_R0coefficients) = S ((S (pfc_index_append_step_R0coefficients)) * r0c)) /\ exists ff_q_pfp_append_step_R0coefficientsentry. r0b = ff_q_pfp_append_step_R0coefficientsentry * S ((S (pfc_index_append_step_R0coefficients)) * r0c) + (pfc_value_append_step_R0coefficients))) /\ ((exists pfc_terms_code_append_step_R0coefficientscoefficient pfc_terms_scale_append_step_R0coefficientscoefficient pfc_natural_sum_append_step_R0coefficientscoefficient. ((forall pfc_index_append_step_R0coefficientscoefficientdiagonal. (exists pfa_gap_append_step_R0coefficientscoefficientdiagonalbound. pfa_gap_append_step_R0coefficientscoefficientdiagonalbound + S (pfc_index_append_step_R0coefficientscoefficientdiagonal) = (S (pfc_index_append_step_R0coefficients))) -> exists pfc_value_append_step_R0coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_R0coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_R0coefficientscoefficientdiagonalentry + S (pfc_value_append_step_R0coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_R0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_R0coefficientscoefficient)) /\ exists ff_q_pfp_append_step_R0coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_R0coefficientscoefficient = ff_q_pfp_append_step_R0coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_R0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_R0coefficientscoefficient) + (pfc_value_append_step_R0coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_R0coefficientscoefficientdiagonalterm pfc_left_append_step_R0coefficientscoefficientdiagonalterm pfc_right_append_step_R0coefficientscoefficientdiagonalterm. (((pfc_index_append_step_R0coefficientscoefficientdiagonal)+pfc_complement_append_step_R0coefficientscoefficientdiagonalterm=(pfc_index_append_step_R0coefficients)) /\ ((((((exists pfa_gap_append_step_R0coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_R0coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_R0coefficientscoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_append_step_R0coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_R0coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_R0coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_R0coefficientscoefficientdiagonal)) * pc)) /\ exists ff_q_pfp_append_step_R0coefficientscoefficientdiagonaltermleftentry. pb = ff_q_pfp_append_step_R0coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_R0coefficientscoefficientdiagonal)) * pc) + (pfc_left_append_step_R0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_R0coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_R0coefficientscoefficientdiagonaltermleftoutside+(N)=(pfc_index_append_step_R0coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_R0coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_R0coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_R0coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_R0coefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_append_step_R0coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_R0coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_R0coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_R0coefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_append_step_R0coefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_append_step_R0coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_R0coefficientscoefficientdiagonalterm)) * cc) + (pfc_right_append_step_R0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_R0coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_R0coefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_append_step_R0coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_R0coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_R0coefficientscoefficientdiagonal)=pfc_left_append_step_R0coefficientscoefficientdiagonalterm*pfc_right_append_step_R0coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_R0coefficientscoefficientsum fs_v_pfc_append_step_R0coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_start. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_R0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_start. fs_u_pfc_append_step_R0coefficientscoefficientsum = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_R0coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_R0coefficientscoefficient) = S ((S (S (pfc_index_append_step_R0coefficients))) * fs_v_pfc_append_step_R0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_R0coefficientscoefficientsum = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_R0coefficients))) * fs_v_pfc_append_step_R0coefficientscoefficientsum) + (pfc_natural_sum_append_step_R0coefficientscoefficient))) /\ forall fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_R0coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_R0coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps = S (pfc_index_append_step_R0coefficients)) -> exists fs_a_pfc_append_step_R0coefficientscoefficientsum_body_steps fs_r_pfc_append_step_R0coefficientscoefficientsum_body_steps fs_s_pfc_append_step_R0coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_R0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_R0coefficientscoefficient)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_R0coefficientscoefficient = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_R0coefficientscoefficient) + (fs_a_pfc_append_step_R0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_R0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_R0coefficientscoefficientsum = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R0coefficientscoefficientsum) + (fs_r_pfc_append_step_R0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_R0coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_R0coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_R0coefficientscoefficientsum = fs_q_pfc_append_step_R0coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_R0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R0coefficientscoefficientsum) + (fs_s_pfc_append_step_R0coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_R0coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_R0coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_R0coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_R0coefficientscoefficientresiduebound. pfa_gap_append_step_R0coefficientscoefficientresiduebound + S (pfc_value_append_step_R0coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_R0coefficientscoefficientresiduecongruence pfa_offset_right_append_step_R0coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_R0coefficientscoefficient) + (p) * pfa_offset_left_append_step_R0coefficientscoefficientresiduecongruence = (pfc_value_append_step_R0coefficients) + (p) * pfa_offset_right_append_step_R0coefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_S0left. (exists fom_gap_pfp_append_step_S0left_index_bound. fom_gap_pfp_append_step_S0left_index_bound + S (fom_index_pfp_append_step_S0left) = L) -> exists fom_value_pfp_append_step_S0left. ((((exists fom_beta_height_pfp_append_step_S0left_entry. fom_beta_height_pfp_append_step_S0left_entry + S (fom_value_pfp_append_step_S0left) = S ((S (fom_index_pfp_append_step_S0left)) * ac)) /\ exists fom_beta_quotient_pfp_append_step_S0left_entry. ab = fom_beta_quotient_pfp_append_step_S0left_entry * S ((S (fom_index_pfp_append_step_S0left)) * ac) + (fom_value_pfp_append_step_S0left))) /\ (exists fom_gap_pfp_append_step_S0left_value_bound. fom_gap_pfp_append_step_S0left_value_bound + S (fom_value_pfp_append_step_S0left) = p))) /\ (((forall fom_index_pfp_append_step_S0right. (exists fom_gap_pfp_append_step_S0right_index_bound. fom_gap_pfp_append_step_S0right_index_bound + S (fom_index_pfp_append_step_S0right) = K0) -> exists fom_value_pfp_append_step_S0right. ((((exists fom_beta_height_pfp_append_step_S0right_entry. fom_beta_height_pfp_append_step_S0right_entry + S (fom_value_pfp_append_step_S0right) = S ((S (fom_index_pfp_append_step_S0right)) * q0c)) /\ exists fom_beta_quotient_pfp_append_step_S0right_entry. q0b = fom_beta_quotient_pfp_append_step_S0right_entry * S ((S (fom_index_pfp_append_step_S0right)) * q0c) + (fom_value_pfp_append_step_S0right))) /\ (exists fom_gap_pfp_append_step_S0right_value_bound. fom_gap_pfp_append_step_S0right_value_bound + S (fom_value_pfp_append_step_S0right) = p))) /\ (((((((L)=0 \/ (K0)=0) /\ (((V0)=0)))) \/ (((~((L)=0)) /\ (((~((K0)=0)) /\ (((L)+(K0)=S (V0)))))))) /\ ((forall pfc_index_append_step_S0coefficients. (exists pfa_gap_append_step_S0coefficientsbound. pfa_gap_append_step_S0coefficientsbound + S (pfc_index_append_step_S0coefficients) = (V0)) -> exists pfc_value_append_step_S0coefficients. ((((exists ff_h_pfp_append_step_S0coefficientsentry. ff_h_pfp_append_step_S0coefficientsentry + S (pfc_value_append_step_S0coefficients) = S ((S (pfc_index_append_step_S0coefficients)) * s0c)) /\ exists ff_q_pfp_append_step_S0coefficientsentry. s0b = ff_q_pfp_append_step_S0coefficientsentry * S ((S (pfc_index_append_step_S0coefficients)) * s0c) + (pfc_value_append_step_S0coefficients))) /\ ((exists pfc_terms_code_append_step_S0coefficientscoefficient pfc_terms_scale_append_step_S0coefficientscoefficient pfc_natural_sum_append_step_S0coefficientscoefficient. ((forall pfc_index_append_step_S0coefficientscoefficientdiagonal. (exists pfa_gap_append_step_S0coefficientscoefficientdiagonalbound. pfa_gap_append_step_S0coefficientscoefficientdiagonalbound + S (pfc_index_append_step_S0coefficientscoefficientdiagonal) = (S (pfc_index_append_step_S0coefficients))) -> exists pfc_value_append_step_S0coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_S0coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_S0coefficientscoefficientdiagonalentry + S (pfc_value_append_step_S0coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_S0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_S0coefficientscoefficient)) /\ exists ff_q_pfp_append_step_S0coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_S0coefficientscoefficient = ff_q_pfp_append_step_S0coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_S0coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_S0coefficientscoefficient) + (pfc_value_append_step_S0coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_S0coefficientscoefficientdiagonalterm pfc_left_append_step_S0coefficientscoefficientdiagonalterm pfc_right_append_step_S0coefficientscoefficientdiagonalterm. (((pfc_index_append_step_S0coefficientscoefficientdiagonal)+pfc_complement_append_step_S0coefficientscoefficientdiagonalterm=(pfc_index_append_step_S0coefficients)) /\ ((((((exists pfa_gap_append_step_S0coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_S0coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_S0coefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_step_S0coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_S0coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_S0coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_S0coefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_step_S0coefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_step_S0coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_S0coefficientscoefficientdiagonal)) * ac) + (pfc_left_append_step_S0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_S0coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_S0coefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_step_S0coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_S0coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_S0coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_S0coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_S0coefficientscoefficientdiagonalterm) = (K0)) /\ ((((exists ff_h_pfp_append_step_S0coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_S0coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_S0coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_S0coefficientscoefficientdiagonalterm)) * q0c)) /\ exists ff_q_pfp_append_step_S0coefficientscoefficientdiagonaltermrightentry. q0b = ff_q_pfp_append_step_S0coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_S0coefficientscoefficientdiagonalterm)) * q0c) + (pfc_right_append_step_S0coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_S0coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_S0coefficientscoefficientdiagonaltermrightoutside+(K0)=(pfc_complement_append_step_S0coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_S0coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_S0coefficientscoefficientdiagonal)=pfc_left_append_step_S0coefficientscoefficientdiagonalterm*pfc_right_append_step_S0coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_S0coefficientscoefficientsum fs_v_pfc_append_step_S0coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_start. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_S0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_start. fs_u_pfc_append_step_S0coefficientscoefficientsum = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_S0coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_S0coefficientscoefficient) = S ((S (S (pfc_index_append_step_S0coefficients))) * fs_v_pfc_append_step_S0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_S0coefficientscoefficientsum = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_S0coefficients))) * fs_v_pfc_append_step_S0coefficientscoefficientsum) + (pfc_natural_sum_append_step_S0coefficientscoefficient))) /\ forall fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_S0coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_S0coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps = S (pfc_index_append_step_S0coefficients)) -> exists fs_a_pfc_append_step_S0coefficientscoefficientsum_body_steps fs_r_pfc_append_step_S0coefficientscoefficientsum_body_steps fs_s_pfc_append_step_S0coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_S0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_S0coefficientscoefficient)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_S0coefficientscoefficient = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_S0coefficientscoefficient) + (fs_a_pfc_append_step_S0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_S0coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_S0coefficientscoefficientsum = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S0coefficientscoefficientsum) + (fs_r_pfc_append_step_S0coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_S0coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_S0coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S0coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_S0coefficientscoefficientsum = fs_q_pfc_append_step_S0coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_S0coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S0coefficientscoefficientsum) + (fs_s_pfc_append_step_S0coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_S0coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_S0coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_S0coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_S0coefficientscoefficientresiduebound. pfa_gap_append_step_S0coefficientscoefficientresiduebound + S (pfc_value_append_step_S0coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_S0coefficientscoefficientresiduecongruence pfa_offset_right_append_step_S0coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_S0coefficientscoefficient) + (p) * pfa_offset_left_append_step_S0coefficientscoefficientresiduecongruence = (pfc_value_append_step_S0coefficients) + (p) * pfa_offset_right_append_step_S0coefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_append_step_actual_induction_hypothesis pfrep_left_append_step_actual_induction_hypothesis pfrep_right_append_step_actual_induction_hypothesis. ((exists pfrep_position_append_step_actual_induction_hypothesisfirst. ((pfrep_position_append_step_actual_induction_hypothesisfirst+S (pfrep_power_append_step_actual_induction_hypothesis)=(U0)) /\ ((((exists ff_h_pfp_append_step_actual_induction_hypothesisfirstentry. ff_h_pfp_append_step_actual_induction_hypothesisfirstentry + S (pfrep_left_append_step_actual_induction_hypothesis) = S ((S (pfrep_position_append_step_actual_induction_hypothesisfirst)) * r0c)) /\ exists ff_q_pfp_append_step_actual_induction_hypothesisfirstentry. r0b = ff_q_pfp_append_step_actual_induction_hypothesisfirstentry * S ((S (pfrep_position_append_step_actual_induction_hypothesisfirst)) * r0c) + (pfrep_left_append_step_actual_induction_hypothesis)))))) \/ (((exists pfrep_gap_append_step_actual_induction_hypothesisfirstoutside. pfrep_gap_append_step_actual_induction_hypothesisfirstoutside+(U0)=(pfrep_power_append_step_actual_induction_hypothesis)) /\ (((pfrep_left_append_step_actual_induction_hypothesis)=0))))) -> ((exists pfrep_position_append_step_actual_induction_hypothesissecond. ((pfrep_position_append_step_actual_induction_hypothesissecond+S (pfrep_power_append_step_actual_induction_hypothesis)=(V0)) /\ ((((exists ff_h_pfp_append_step_actual_induction_hypothesissecondentry. ff_h_pfp_append_step_actual_induction_hypothesissecondentry + S (pfrep_right_append_step_actual_induction_hypothesis) = S ((S (pfrep_position_append_step_actual_induction_hypothesissecond)) * s0c)) /\ exists ff_q_pfp_append_step_actual_induction_hypothesissecondentry. s0b = ff_q_pfp_append_step_actual_induction_hypothesissecondentry * S ((S (pfrep_position_append_step_actual_induction_hypothesissecond)) * s0c) + (pfrep_right_append_step_actual_induction_hypothesis)))))) \/ (((exists pfrep_gap_append_step_actual_induction_hypothesissecondoutside. pfrep_gap_append_step_actual_induction_hypothesissecondoutside+(V0)=(pfrep_power_append_step_actual_induction_hypothesis)) /\ (((pfrep_right_append_step_actual_induction_hypothesis)=0))))) -> pfrep_left_append_step_actual_induction_hypothesis=pfrep_right_append_step_actual_induction_hypothesis) -> (forall mdr_i_pfp_append_step_prefix mdr_a_pfp_append_step_prefix. (exists mdr_gap_pfp_append_step_prefixb. mdr_gap_pfp_append_step_prefixb + S (mdr_i_pfp_append_step_prefix) = (J)) -> (((exists ff_h_mdr_pfp_append_step_prefixo. ff_h_mdr_pfp_append_step_prefixo + S (mdr_a_pfp_append_step_prefix) = S ((S (mdr_i_pfp_append_step_prefix)) * cc)) /\ exists ff_q_mdr_pfp_append_step_prefixo. cb = ff_q_mdr_pfp_append_step_prefixo * S ((S (mdr_i_pfp_append_step_prefix)) * cc) + (mdr_a_pfp_append_step_prefix))) -> (((exists ff_h_mdr_pfp_append_step_prefixn. ff_h_mdr_pfp_append_step_prefixn + S (mdr_a_pfp_append_step_prefix) = S ((S (mdr_i_pfp_append_step_prefix)) * dc)) /\ exists ff_q_mdr_pfp_append_step_prefixn. db = ff_q_mdr_pfp_append_step_prefixn * S ((S (mdr_i_pfp_append_step_prefix)) * dc) + (mdr_a_pfp_append_step_prefix)))) -> (((exists ff_h_pfp_append_step_last. ff_h_pfp_append_step_last + S (c) = S ((S (J)) * dc)) /\ exists ff_q_pfp_append_step_last. db = ff_q_pfp_append_step_last * S ((S (J)) * dc) + (c))) -> (((forall fom_index_pfp_append_step_Q1left. (exists fom_gap_pfp_append_step_Q1left_index_bound. fom_gap_pfp_append_step_Q1left_index_bound + S (fom_index_pfp_append_step_Q1left) = M) -> exists fom_value_pfp_append_step_Q1left. ((((exists fom_beta_height_pfp_append_step_Q1left_entry. fom_beta_height_pfp_append_step_Q1left_entry + S (fom_value_pfp_append_step_Q1left) = S ((S (fom_index_pfp_append_step_Q1left)) * bc)) /\ exists fom_beta_quotient_pfp_append_step_Q1left_entry. bb = fom_beta_quotient_pfp_append_step_Q1left_entry * S ((S (fom_index_pfp_append_step_Q1left)) * bc) + (fom_value_pfp_append_step_Q1left))) /\ (exists fom_gap_pfp_append_step_Q1left_value_bound. fom_gap_pfp_append_step_Q1left_value_bound + S (fom_value_pfp_append_step_Q1left) = p))) /\ (((forall fom_index_pfp_append_step_Q1right. (exists fom_gap_pfp_append_step_Q1right_index_bound. fom_gap_pfp_append_step_Q1right_index_bound + S (fom_index_pfp_append_step_Q1right) = S J) -> exists fom_value_pfp_append_step_Q1right. ((((exists fom_beta_height_pfp_append_step_Q1right_entry. fom_beta_height_pfp_append_step_Q1right_entry + S (fom_value_pfp_append_step_Q1right) = S ((S (fom_index_pfp_append_step_Q1right)) * dc)) /\ exists fom_beta_quotient_pfp_append_step_Q1right_entry. db = fom_beta_quotient_pfp_append_step_Q1right_entry * S ((S (fom_index_pfp_append_step_Q1right)) * dc) + (fom_value_pfp_append_step_Q1right))) /\ (exists fom_gap_pfp_append_step_Q1right_value_bound. fom_gap_pfp_append_step_Q1right_value_bound + S (fom_value_pfp_append_step_Q1right) = p))) /\ (((((((M)=0 \/ (S J)=0) /\ (((K1)=0)))) \/ (((~((M)=0)) /\ (((~((S J)=0)) /\ (((M)+(S J)=S (K1)))))))) /\ ((forall pfc_index_append_step_Q1coefficients. (exists pfa_gap_append_step_Q1coefficientsbound. pfa_gap_append_step_Q1coefficientsbound + S (pfc_index_append_step_Q1coefficients) = (K1)) -> exists pfc_value_append_step_Q1coefficients. ((((exists ff_h_pfp_append_step_Q1coefficientsentry. ff_h_pfp_append_step_Q1coefficientsentry + S (pfc_value_append_step_Q1coefficients) = S ((S (pfc_index_append_step_Q1coefficients)) * q1c)) /\ exists ff_q_pfp_append_step_Q1coefficientsentry. q1b = ff_q_pfp_append_step_Q1coefficientsentry * S ((S (pfc_index_append_step_Q1coefficients)) * q1c) + (pfc_value_append_step_Q1coefficients))) /\ ((exists pfc_terms_code_append_step_Q1coefficientscoefficient pfc_terms_scale_append_step_Q1coefficientscoefficient pfc_natural_sum_append_step_Q1coefficientscoefficient. ((forall pfc_index_append_step_Q1coefficientscoefficientdiagonal. (exists pfa_gap_append_step_Q1coefficientscoefficientdiagonalbound. pfa_gap_append_step_Q1coefficientscoefficientdiagonalbound + S (pfc_index_append_step_Q1coefficientscoefficientdiagonal) = (S (pfc_index_append_step_Q1coefficients))) -> exists pfc_value_append_step_Q1coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_Q1coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_Q1coefficientscoefficientdiagonalentry + S (pfc_value_append_step_Q1coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q1coefficientscoefficient)) /\ exists ff_q_pfp_append_step_Q1coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_Q1coefficientscoefficient = ff_q_pfp_append_step_Q1coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q1coefficientscoefficient) + (pfc_value_append_step_Q1coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm pfc_left_append_step_Q1coefficientscoefficientdiagonalterm pfc_right_append_step_Q1coefficientscoefficientdiagonalterm. (((pfc_index_append_step_Q1coefficientscoefficientdiagonal)+pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm=(pfc_index_append_step_Q1coefficients)) /\ ((((((exists pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_Q1coefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_Q1coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * bc)) /\ exists ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry. bb = ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * bc) + (pfc_left_append_step_Q1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_append_step_Q1coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_Q1coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm) = (S J)) /\ ((((exists ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_Q1coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm)) * dc) + (pfc_right_append_step_Q1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermrightoutside+(S J)=(pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_Q1coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_Q1coefficientscoefficientdiagonal)=pfc_left_append_step_Q1coefficientscoefficientdiagonalterm*pfc_right_append_step_Q1coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_Q1coefficientscoefficientsum fs_v_pfc_append_step_Q1coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_start. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_start. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_Q1coefficientscoefficient) = S ((S (S (pfc_index_append_step_Q1coefficients))) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_Q1coefficients))) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (pfc_natural_sum_append_step_Q1coefficientscoefficient))) /\ forall fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_Q1coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_Q1coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps = S (pfc_index_append_step_Q1coefficients)) -> exists fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q1coefficientscoefficient)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_Q1coefficientscoefficient = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q1coefficientscoefficient) + (fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_Q1coefficientscoefficientresiduebound. pfa_gap_append_step_Q1coefficientscoefficientresiduebound + S (pfc_value_append_step_Q1coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_Q1coefficientscoefficientresiduecongruence pfa_offset_right_append_step_Q1coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_Q1coefficientscoefficient) + (p) * pfa_offset_left_append_step_Q1coefficientscoefficientresiduecongruence = (pfc_value_append_step_Q1coefficients) + (p) * pfa_offset_right_append_step_Q1coefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_R1left. (exists fom_gap_pfp_append_step_R1left_index_bound. fom_gap_pfp_append_step_R1left_index_bound + S (fom_index_pfp_append_step_R1left) = N) -> exists fom_value_pfp_append_step_R1left. ((((exists fom_beta_height_pfp_append_step_R1left_entry. fom_beta_height_pfp_append_step_R1left_entry + S (fom_value_pfp_append_step_R1left) = S ((S (fom_index_pfp_append_step_R1left)) * pc)) /\ exists fom_beta_quotient_pfp_append_step_R1left_entry. pb = fom_beta_quotient_pfp_append_step_R1left_entry * S ((S (fom_index_pfp_append_step_R1left)) * pc) + (fom_value_pfp_append_step_R1left))) /\ (exists fom_gap_pfp_append_step_R1left_value_bound. fom_gap_pfp_append_step_R1left_value_bound + S (fom_value_pfp_append_step_R1left) = p))) /\ (((forall fom_index_pfp_append_step_R1right. (exists fom_gap_pfp_append_step_R1right_index_bound. fom_gap_pfp_append_step_R1right_index_bound + S (fom_index_pfp_append_step_R1right) = S J) -> exists fom_value_pfp_append_step_R1right. ((((exists fom_beta_height_pfp_append_step_R1right_entry. fom_beta_height_pfp_append_step_R1right_entry + S (fom_value_pfp_append_step_R1right) = S ((S (fom_index_pfp_append_step_R1right)) * dc)) /\ exists fom_beta_quotient_pfp_append_step_R1right_entry. db = fom_beta_quotient_pfp_append_step_R1right_entry * S ((S (fom_index_pfp_append_step_R1right)) * dc) + (fom_value_pfp_append_step_R1right))) /\ (exists fom_gap_pfp_append_step_R1right_value_bound. fom_gap_pfp_append_step_R1right_value_bound + S (fom_value_pfp_append_step_R1right) = p))) /\ (((((((N)=0 \/ (S J)=0) /\ (((U1)=0)))) \/ (((~((N)=0)) /\ (((~((S J)=0)) /\ (((N)+(S J)=S (U1)))))))) /\ ((forall pfc_index_append_step_R1coefficients. (exists pfa_gap_append_step_R1coefficientsbound. pfa_gap_append_step_R1coefficientsbound + S (pfc_index_append_step_R1coefficients) = (U1)) -> exists pfc_value_append_step_R1coefficients. ((((exists ff_h_pfp_append_step_R1coefficientsentry. ff_h_pfp_append_step_R1coefficientsentry + S (pfc_value_append_step_R1coefficients) = S ((S (pfc_index_append_step_R1coefficients)) * r1c)) /\ exists ff_q_pfp_append_step_R1coefficientsentry. r1b = ff_q_pfp_append_step_R1coefficientsentry * S ((S (pfc_index_append_step_R1coefficients)) * r1c) + (pfc_value_append_step_R1coefficients))) /\ ((exists pfc_terms_code_append_step_R1coefficientscoefficient pfc_terms_scale_append_step_R1coefficientscoefficient pfc_natural_sum_append_step_R1coefficientscoefficient. ((forall pfc_index_append_step_R1coefficientscoefficientdiagonal. (exists pfa_gap_append_step_R1coefficientscoefficientdiagonalbound. pfa_gap_append_step_R1coefficientscoefficientdiagonalbound + S (pfc_index_append_step_R1coefficientscoefficientdiagonal) = (S (pfc_index_append_step_R1coefficients))) -> exists pfc_value_append_step_R1coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_R1coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_R1coefficientscoefficientdiagonalentry + S (pfc_value_append_step_R1coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_R1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_R1coefficientscoefficient)) /\ exists ff_q_pfp_append_step_R1coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_R1coefficientscoefficient = ff_q_pfp_append_step_R1coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_R1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_R1coefficientscoefficient) + (pfc_value_append_step_R1coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_R1coefficientscoefficientdiagonalterm pfc_left_append_step_R1coefficientscoefficientdiagonalterm pfc_right_append_step_R1coefficientscoefficientdiagonalterm. (((pfc_index_append_step_R1coefficientscoefficientdiagonal)+pfc_complement_append_step_R1coefficientscoefficientdiagonalterm=(pfc_index_append_step_R1coefficients)) /\ ((((((exists pfa_gap_append_step_R1coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_R1coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_R1coefficientscoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_append_step_R1coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_R1coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_R1coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_R1coefficientscoefficientdiagonal)) * pc)) /\ exists ff_q_pfp_append_step_R1coefficientscoefficientdiagonaltermleftentry. pb = ff_q_pfp_append_step_R1coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_R1coefficientscoefficientdiagonal)) * pc) + (pfc_left_append_step_R1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_R1coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_R1coefficientscoefficientdiagonaltermleftoutside+(N)=(pfc_index_append_step_R1coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_R1coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_R1coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_R1coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_R1coefficientscoefficientdiagonalterm) = (S J)) /\ ((((exists ff_h_pfp_append_step_R1coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_R1coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_R1coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_R1coefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_step_R1coefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_append_step_R1coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_R1coefficientscoefficientdiagonalterm)) * dc) + (pfc_right_append_step_R1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_R1coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_R1coefficientscoefficientdiagonaltermrightoutside+(S J)=(pfc_complement_append_step_R1coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_R1coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_R1coefficientscoefficientdiagonal)=pfc_left_append_step_R1coefficientscoefficientdiagonalterm*pfc_right_append_step_R1coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_R1coefficientscoefficientsum fs_v_pfc_append_step_R1coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_start. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_R1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_start. fs_u_pfc_append_step_R1coefficientscoefficientsum = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_R1coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_R1coefficientscoefficient) = S ((S (S (pfc_index_append_step_R1coefficients))) * fs_v_pfc_append_step_R1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_R1coefficientscoefficientsum = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_R1coefficients))) * fs_v_pfc_append_step_R1coefficientscoefficientsum) + (pfc_natural_sum_append_step_R1coefficientscoefficient))) /\ forall fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_R1coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_R1coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps = S (pfc_index_append_step_R1coefficients)) -> exists fs_a_pfc_append_step_R1coefficientscoefficientsum_body_steps fs_r_pfc_append_step_R1coefficientscoefficientsum_body_steps fs_s_pfc_append_step_R1coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_R1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_R1coefficientscoefficient)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_R1coefficientscoefficient = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_R1coefficientscoefficient) + (fs_a_pfc_append_step_R1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_R1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_R1coefficientscoefficientsum = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R1coefficientscoefficientsum) + (fs_r_pfc_append_step_R1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_R1coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_R1coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_R1coefficientscoefficientsum = fs_q_pfc_append_step_R1coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_R1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_R1coefficientscoefficientsum) + (fs_s_pfc_append_step_R1coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_R1coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_R1coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_R1coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_R1coefficientscoefficientresiduebound. pfa_gap_append_step_R1coefficientscoefficientresiduebound + S (pfc_value_append_step_R1coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_R1coefficientscoefficientresiduecongruence pfa_offset_right_append_step_R1coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_R1coefficientscoefficient) + (p) * pfa_offset_left_append_step_R1coefficientscoefficientresiduecongruence = (pfc_value_append_step_R1coefficients) + (p) * pfa_offset_right_append_step_R1coefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_step_S1left. (exists fom_gap_pfp_append_step_S1left_index_bound. fom_gap_pfp_append_step_S1left_index_bound + S (fom_index_pfp_append_step_S1left) = L) -> exists fom_value_pfp_append_step_S1left. ((((exists fom_beta_height_pfp_append_step_S1left_entry. fom_beta_height_pfp_append_step_S1left_entry + S (fom_value_pfp_append_step_S1left) = S ((S (fom_index_pfp_append_step_S1left)) * ac)) /\ exists fom_beta_quotient_pfp_append_step_S1left_entry. ab = fom_beta_quotient_pfp_append_step_S1left_entry * S ((S (fom_index_pfp_append_step_S1left)) * ac) + (fom_value_pfp_append_step_S1left))) /\ (exists fom_gap_pfp_append_step_S1left_value_bound. fom_gap_pfp_append_step_S1left_value_bound + S (fom_value_pfp_append_step_S1left) = p))) /\ (((forall fom_index_pfp_append_step_S1right. (exists fom_gap_pfp_append_step_S1right_index_bound. fom_gap_pfp_append_step_S1right_index_bound + S (fom_index_pfp_append_step_S1right) = K1) -> exists fom_value_pfp_append_step_S1right. ((((exists fom_beta_height_pfp_append_step_S1right_entry. fom_beta_height_pfp_append_step_S1right_entry + S (fom_value_pfp_append_step_S1right) = S ((S (fom_index_pfp_append_step_S1right)) * q1c)) /\ exists fom_beta_quotient_pfp_append_step_S1right_entry. q1b = fom_beta_quotient_pfp_append_step_S1right_entry * S ((S (fom_index_pfp_append_step_S1right)) * q1c) + (fom_value_pfp_append_step_S1right))) /\ (exists fom_gap_pfp_append_step_S1right_value_bound. fom_gap_pfp_append_step_S1right_value_bound + S (fom_value_pfp_append_step_S1right) = p))) /\ (((((((L)=0 \/ (K1)=0) /\ (((V1)=0)))) \/ (((~((L)=0)) /\ (((~((K1)=0)) /\ (((L)+(K1)=S (V1)))))))) /\ ((forall pfc_index_append_step_S1coefficients. (exists pfa_gap_append_step_S1coefficientsbound. pfa_gap_append_step_S1coefficientsbound + S (pfc_index_append_step_S1coefficients) = (V1)) -> exists pfc_value_append_step_S1coefficients. ((((exists ff_h_pfp_append_step_S1coefficientsentry. ff_h_pfp_append_step_S1coefficientsentry + S (pfc_value_append_step_S1coefficients) = S ((S (pfc_index_append_step_S1coefficients)) * s1c)) /\ exists ff_q_pfp_append_step_S1coefficientsentry. s1b = ff_q_pfp_append_step_S1coefficientsentry * S ((S (pfc_index_append_step_S1coefficients)) * s1c) + (pfc_value_append_step_S1coefficients))) /\ ((exists pfc_terms_code_append_step_S1coefficientscoefficient pfc_terms_scale_append_step_S1coefficientscoefficient pfc_natural_sum_append_step_S1coefficientscoefficient. ((forall pfc_index_append_step_S1coefficientscoefficientdiagonal. (exists pfa_gap_append_step_S1coefficientscoefficientdiagonalbound. pfa_gap_append_step_S1coefficientscoefficientdiagonalbound + S (pfc_index_append_step_S1coefficientscoefficientdiagonal) = (S (pfc_index_append_step_S1coefficients))) -> exists pfc_value_append_step_S1coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_S1coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_S1coefficientscoefficientdiagonalentry + S (pfc_value_append_step_S1coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_S1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_S1coefficientscoefficient)) /\ exists ff_q_pfp_append_step_S1coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_S1coefficientscoefficient = ff_q_pfp_append_step_S1coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_S1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_S1coefficientscoefficient) + (pfc_value_append_step_S1coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_S1coefficientscoefficientdiagonalterm pfc_left_append_step_S1coefficientscoefficientdiagonalterm pfc_right_append_step_S1coefficientscoefficientdiagonalterm. (((pfc_index_append_step_S1coefficientscoefficientdiagonal)+pfc_complement_append_step_S1coefficientscoefficientdiagonalterm=(pfc_index_append_step_S1coefficients)) /\ ((((((exists pfa_gap_append_step_S1coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_S1coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_S1coefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_step_S1coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_S1coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_S1coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_S1coefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_step_S1coefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_step_S1coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_S1coefficientscoefficientdiagonal)) * ac) + (pfc_left_append_step_S1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_S1coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_S1coefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_step_S1coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_S1coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_S1coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_S1coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_S1coefficientscoefficientdiagonalterm) = (K1)) /\ ((((exists ff_h_pfp_append_step_S1coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_S1coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_S1coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_S1coefficientscoefficientdiagonalterm)) * q1c)) /\ exists ff_q_pfp_append_step_S1coefficientscoefficientdiagonaltermrightentry. q1b = ff_q_pfp_append_step_S1coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_S1coefficientscoefficientdiagonalterm)) * q1c) + (pfc_right_append_step_S1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_S1coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_S1coefficientscoefficientdiagonaltermrightoutside+(K1)=(pfc_complement_append_step_S1coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_S1coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_S1coefficientscoefficientdiagonal)=pfc_left_append_step_S1coefficientscoefficientdiagonalterm*pfc_right_append_step_S1coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_S1coefficientscoefficientsum fs_v_pfc_append_step_S1coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_start. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_S1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_start. fs_u_pfc_append_step_S1coefficientscoefficientsum = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_S1coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_S1coefficientscoefficient) = S ((S (S (pfc_index_append_step_S1coefficients))) * fs_v_pfc_append_step_S1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_S1coefficientscoefficientsum = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_S1coefficients))) * fs_v_pfc_append_step_S1coefficientscoefficientsum) + (pfc_natural_sum_append_step_S1coefficientscoefficient))) /\ forall fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_S1coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_S1coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps = S (pfc_index_append_step_S1coefficients)) -> exists fs_a_pfc_append_step_S1coefficientscoefficientsum_body_steps fs_r_pfc_append_step_S1coefficientscoefficientsum_body_steps fs_s_pfc_append_step_S1coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_S1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_S1coefficientscoefficient)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_S1coefficientscoefficient = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_S1coefficientscoefficient) + (fs_a_pfc_append_step_S1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_S1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_S1coefficientscoefficientsum = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S1coefficientscoefficientsum) + (fs_r_pfc_append_step_S1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_S1coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_S1coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_S1coefficientscoefficientsum = fs_q_pfc_append_step_S1coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_S1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_S1coefficientscoefficientsum) + (fs_s_pfc_append_step_S1coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_S1coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_S1coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_S1coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_S1coefficientscoefficientresiduebound. pfa_gap_append_step_S1coefficientscoefficientresiduebound + S (pfc_value_append_step_S1coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_S1coefficientscoefficientresiduecongruence pfa_offset_right_append_step_S1coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_S1coefficientscoefficient) + (p) * pfa_offset_left_append_step_S1coefficientscoefficientresiduecongruence = (pfc_value_append_step_S1coefficients) + (p) * pfa_offset_right_append_step_S1coefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_append_step_result pfrep_left_append_step_result pfrep_right_append_step_result. ((exists pfrep_position_append_step_resultfirst. ((pfrep_position_append_step_resultfirst+S (pfrep_power_append_step_result)=(U1)) /\ ((((exists ff_h_pfp_append_step_resultfirstentry. ff_h_pfp_append_step_resultfirstentry + S (pfrep_left_append_step_result) = S ((S (pfrep_position_append_step_resultfirst)) * r1c)) /\ exists ff_q_pfp_append_step_resultfirstentry. r1b = ff_q_pfp_append_step_resultfirstentry * S ((S (pfrep_position_append_step_resultfirst)) * r1c) + (pfrep_left_append_step_result)))))) \/ (((exists pfrep_gap_append_step_resultfirstoutside. pfrep_gap_append_step_resultfirstoutside+(U1)=(pfrep_power_append_step_result)) /\ (((pfrep_left_append_step_result)=0))))) -> ((exists pfrep_position_append_step_resultsecond. ((pfrep_position_append_step_resultsecond+S (pfrep_power_append_step_result)=(V1)) /\ ((((exists ff_h_pfp_append_step_resultsecondentry. ff_h_pfp_append_step_resultsecondentry + S (pfrep_right_append_step_result) = S ((S (pfrep_position_append_step_resultsecond)) * s1c)) /\ exists ff_q_pfp_append_step_resultsecondentry. s1b = ff_q_pfp_append_step_resultsecondentry * S ((S (pfrep_position_append_step_resultsecond)) * s1c) + (pfrep_right_append_step_result)))))) \/ (((exists pfrep_gap_append_step_resultsecondoutside. pfrep_gap_append_step_resultsecondoutside+(V1)=(pfrep_power_append_step_result)) /\ (((pfrep_right_append_step_result)=0))))) -> pfrep_left_append_step_result=pfrep_right_append_step_result)Constructive proof overview
Generated structural guide
An actual formal-coefficient associativity hypothesis for one rightmost prefix extends through one genuine appended coefficient. Every old and new product is an actual proper-length convolution; the proof derives the canonical appended coefficient bound, constructs three real shift/scale/pad/add alignments and a real intermediate product, and concludes only the next formal equivalence. Empty factors are retained, no successor product-length identity is assumed, and the induction step alone is not full associativity.
The unchanged tactic script uses 14 declared prerequisites and contains 487 exact native proof lines.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
prime_nonzero Alpha theorem; checked-use authorized matrix_rank_bounded_prefix_value Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized prime_field_polynomial_convolution_bounded Alpha theorem; checked-use authorized PG001D prime_field_polynomial_shift_scale_aligned_sum_exists prime_field_polynomial_add_bounded Alpha theorem; checked-use authorized polynomial_product_length_exists Alpha theorem; checked-use authorized prime_field_polynomial_convolution_at_length_exists Alpha theorem; checked-use authorized PG0021 prime_field_polynomial_convolution_shift_scale_aligned_equivalent PG001E prime_field_polynomial_convolution_right_append_equivalent prime_field_polynomial_convolution_equivalent_congruent_right Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_transitive Alpha theorem; checked-use authorized PG0022 prime_field_polynomial_shift_scale_aligned_congruent prime_field_polynomial_equivalent_symmetric Alpha theorem; checked-use authorizedDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (4)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–20
03Fix variables and assumptionsL21–30
04Fix variables and assumptionsL31–40
05Fix variables and assumptionsL41–45
06Establish hp0L46–51
07Establish hABcopyL52–53
Establish this local claim before using it. It is not an additional assumption.
- L52
have hABcopy : FpPolyProduct(p,ab,ac,L,bb,bc,M,pb,pc,N)Definitions: FpPolyProduct - L53
exact hAB
08Separate the logical casesL54–56
09Establish hQ1copyL57–58
Establish this local claim before using it. It is not an additional assumption.
- L57
have hQ1copy : FpPolyProduct(p,bb,bc,M,db,dc,S J,q1b,q1c,K1)Definitions: FpPolyProduct - L58
exact hQ1
10Separate the logical casesL59–61
11Establish hcL62–71
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank bounded prefix value.
- L62
have hc : exists pfa_gap_append_step_scalar_bound. pfa_gap_append_step_scalar_bound + S (c) = (p) - L63
specialize matrix_rank_bounded_prefix_value (db) - L64
specialize matrix_rank_bounded_prefix_value (dc) - L65
specialize matrix_rank_bounded_prefix_value (S J) - L66
specialize matrix_rank_bounded_prefix_value (p) - L67
specialize matrix_rank_bounded_prefix_value (J) - L68
specialize matrix_rank_bounded_prefix_value (c) - L69
apply matrix_rank_bounded_prefix_value - L70
exact hQ1copy_right_left - L71
specialize le_refl (S J)
12Use earlier factsL72–73
13Establish hPboundL74–83
Establish this local claim before using it. It is not an additional assumption.
- L74
have hPbound : BetaPrefixInto(pb,pc,N,p)Definitions: BetaPrefixInto - L75
specialize prime_field_polynomial_convolution_bounded (p) - L76
specialize prime_field_polynomial_convolution_bounded (ab) - L77
specialize prime_field_polynomial_convolution_bounded (ac) - L78
specialize prime_field_polynomial_convolution_bounded (L) - L79
specialize prime_field_polynomial_convolution_bounded (bb) - L80
specialize prime_field_polynomial_convolution_bounded (bc) - L81
specialize prime_field_polynomial_convolution_bounded (M) - L82
specialize prime_field_polynomial_convolution_bounded (pb) - L83
specialize prime_field_polynomial_convolution_bounded (pc)
14Use earlier factsL84–86
15Establish hQ0boundL87–96
Establish this local claim before using it. It is not an additional assumption.
- L87
have hQ0bound : BetaPrefixInto(q0b,q0c,K0,p)Definitions: BetaPrefixInto - L88
specialize prime_field_polynomial_convolution_bounded (p) - L89
specialize prime_field_polynomial_convolution_bounded (bb) - L90
specialize prime_field_polynomial_convolution_bounded (bc) - L91
specialize prime_field_polynomial_convolution_bounded (M) - L92
specialize prime_field_polynomial_convolution_bounded (cb) - L93
specialize prime_field_polynomial_convolution_bounded (cc) - L94
specialize prime_field_polynomial_convolution_bounded (J) - L95
specialize prime_field_polynomial_convolution_bounded (q0b) - L96
specialize prime_field_polynomial_convolution_bounded (q0c)
16Use earlier factsL97–99
17Establish hR0boundL100–109
Establish this local claim before using it. It is not an additional assumption.
- L100
have hR0bound : BetaPrefixInto(r0b,r0c,U0,p)Definitions: BetaPrefixInto - L101
specialize prime_field_polynomial_convolution_bounded (p) - L102
specialize prime_field_polynomial_convolution_bounded (pb) - L103
specialize prime_field_polynomial_convolution_bounded (pc) - L104
specialize prime_field_polynomial_convolution_bounded (N) - L105
specialize prime_field_polynomial_convolution_bounded (cb) - L106
specialize prime_field_polynomial_convolution_bounded (cc) - L107
specialize prime_field_polynomial_convolution_bounded (J) - L108
specialize prime_field_polynomial_convolution_bounded (r0b) - L109
specialize prime_field_polynomial_convolution_bounded (r0c)
18Use earlier factsL110–112
19Establish hS0boundL113–122
Establish this local claim before using it. It is not an additional assumption.
- L113
have hS0bound : BetaPrefixInto(s0b,s0c,V0,p)Definitions: BetaPrefixInto - L114
specialize prime_field_polynomial_convolution_bounded (p) - L115
specialize prime_field_polynomial_convolution_bounded (ab) - L116
specialize prime_field_polynomial_convolution_bounded (ac) - L117
specialize prime_field_polynomial_convolution_bounded (L) - L118
specialize prime_field_polynomial_convolution_bounded (q0b) - L119
specialize prime_field_polynomial_convolution_bounded (q0c) - L120
specialize prime_field_polynomial_convolution_bounded (K0) - L121
specialize prime_field_polynomial_convolution_bounded (s0b) - L122
specialize prime_field_polynomial_convolution_bounded (s0c)
20Use earlier factsL123–125
21Establish hYalignL126–135
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial shift scale aligned sum exists.
- L126
have hYalign : ∃ ub. ∃ uc. ∃ vb. ∃ vc. ∃ UPb. ∃ UPc. ∃ VPb. ∃ VPc. ∃ zb. ∃ zc. PolynomialShift(s0b,s0c,V0,ub,uc) ∧ (FpPolyScale(p,c,pb,pc,vb,vc,N) ∧ (PolynomialLeftPad(ub,uc,S V0,N,UPb,UPc) ∧ (PolynomialLeftPad(vb,vc,N,S V0,VPb,VPc) ∧ FpPolyAdd(p,UPb,UPc,VPb,VPc,zb,zc,N + S V0))))Definitions: FpPolyAddFpPolyScalePolynomialLeftPadPolynomialShift - L127
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (p) - L128
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (c) - L129
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (pb) - L130
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (pc) - L131
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (N) - L132
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (s0b) - L133
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (s0c) - L134
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (V0) - L135
apply prime_field_polynomial_shift_scale_aligned_sum_exists
22Use earlier factsL136–139
23Separate the logical casesL140–149
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L140
cases hYalign - L141
cases hYalign_witness - L142
cases hYalign_witness_witness - L143
cases hYalign_witness_witness_witness - L144
cases hYalign_witness_witness_witness_witness - L145
cases hYalign_witness_witness_witness_witness_witness - L146
cases hYalign_witness_witness_witness_witness_witness_witness - L147
cases hYalign_witness_witness_witness_witness_witness_witness_witness - L148
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness - L149
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness
24Separate the logical casesL150–153
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L150
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness - L151
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right - L152
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right - L153
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
25Establish hS_totalL154–154
Establish this local claim before using it. It is not an additional assumption.
- L154
have hS_total : PolynomialEquivalent(s1b,s1c,V1,x8,x9,N + S V0)Definitions: PolynomialEquivalent
26Establish hZalignL155–164
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial shift scale aligned sum exists.
- L155
have hZalign : ∃ ub. ∃ uc. ∃ vb. ∃ vc. ∃ UPb. ∃ UPc. ∃ VPb. ∃ VPc. ∃ zb. ∃ zc. PolynomialShift(q0b,q0c,K0,ub,uc) ∧ (FpPolyScale(p,c,bb,bc,vb,vc,M) ∧ (PolynomialLeftPad(ub,uc,S K0,M,UPb,UPc) ∧ (PolynomialLeftPad(vb,vc,M,S K0,VPb,VPc) ∧ FpPolyAdd(p,UPb,UPc,VPb,VPc,zb,zc,M + S K0))))Definitions: FpPolyAddFpPolyScalePolynomialLeftPadPolynomialShift - L156
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (p) - L157
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (c) - L158
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (bb) - L159
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (bc) - L160
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (M) - L161
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (q0b) - L162
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (q0c) - L163
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (K0) - L164
apply prime_field_polynomial_shift_scale_aligned_sum_exists
27Use earlier factsL165–168
28Separate the logical casesL169–178
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L169
cases hZalign - L170
cases hZalign_witness - L171
cases hZalign_witness_witness - L172
cases hZalign_witness_witness_witness - L173
cases hZalign_witness_witness_witness_witness - L174
cases hZalign_witness_witness_witness_witness_witness - L175
cases hZalign_witness_witness_witness_witness_witness_witness - L176
cases hZalign_witness_witness_witness_witness_witness_witness_witness - L177
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness - L178
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness
29Separate the logical casesL179–182
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L179
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness - L180
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right - L181
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right - L182
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
30Establish hZboundsL183–192
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial add bounded.
- L183
have hZbounds : BetaPrefixInto(x14,x15,M + S K0,p) ∧ (BetaPrefixInto(x16,x17,M + S K0,p) ∧ BetaPrefixInto(x18,x19,M + S K0,p))Definitions: BetaPrefixInto - L184
specialize prime_field_polynomial_add_bounded (p) - L185
specialize prime_field_polynomial_add_bounded (x14) - L186
specialize prime_field_polynomial_add_bounded (x15) - L187
specialize prime_field_polynomial_add_bounded (x16) - L188
specialize prime_field_polynomial_add_bounded (x17) - L189
specialize prime_field_polynomial_add_bounded (x18) - L190
specialize prime_field_polynomial_add_bounded (x19) - L191
specialize prime_field_polynomial_add_bounded (M+S K0) - L192
apply prime_field_polynomial_add_bounded
31Use earlier factsL193–193
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L193
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
32Separate the logical casesL194–195
33Establish hZlengthL196–199
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.
34Separate the logical casesL200–200
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L200
cases hZlength
35Establish hAZL201–210
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.
- L201
have hAZ : ∃ mb. ∃ mc. FpPolyProduct(p,ab,ac,L,x18,x19,M + S K0,mb,mc,x20)Definitions: FpPolyProduct - L202
specialize prime_field_polynomial_convolution_at_length_exists (p) - L203
specialize prime_field_polynomial_convolution_at_length_exists (ab) - L204
specialize prime_field_polynomial_convolution_at_length_exists (ac) - L205
specialize prime_field_polynomial_convolution_at_length_exists (L) - L206
specialize prime_field_polynomial_convolution_at_length_exists (x18) - L207
specialize prime_field_polynomial_convolution_at_length_exists (x19) - L208
specialize prime_field_polynomial_convolution_at_length_exists (M+S K0) - L209
specialize prime_field_polynomial_convolution_at_length_exists (x20) - L210
apply prime_field_polynomial_convolution_at_length_exists
36Use earlier factsL211–214
37Separate the logical casesL215–216
38Establish hhelper_equalL217–226
Establish this local claim before using it. It is not an additional assumption.
- L217
have hhelper_equal : PolynomialEquivalent(x21,x22,x20,x8,x9,N + S V0)Definitions: PolynomialEquivalent - L218
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (p) - L219
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (c) - L220
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (ab) - L221
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (ac) - L222
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (L) - L223
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (bb) - L224
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (bc) - L225
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (M) - L226
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (pb)
39Use earlier factsL227–236
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L227
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (pc) - L228
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (N) - L229
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (q0b) - L230
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (q0c) - L231
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (K0) - L232
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (s0b) - L233
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (s0c) - L234
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (V0) - L235
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x10) - L236
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x11)
40Use earlier factsL237–246
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L237
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x12) - L238
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x13) - L239
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x14) - L240
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x15) - L241
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x16) - L242
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x17) - L243
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x18) - L244
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x19) - L245
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x21) - L246
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x22)
41Use earlier factsL247–256
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L247
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x20) - L248
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x) - L249
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x1) - L250
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x2) - L251
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x3) - L252
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x4) - L253
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x5) - L254
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x6) - L255
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x7) - L256
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x8)
42Use earlier factsL257–266
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L257
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x9) - L258
apply prime_field_polynomial_convolution_shift_scale_aligned_equivalent - L259
exact hp - L260
exact hAB - L261
exact hS0 - L262
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - L263
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - L264
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - L265
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - L266
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
43Use earlier factsL267–272
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L267
exact hAZ_witness_witness - L268
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - L269
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - L270
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - L271
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - L272
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
44Establish hQ_appendL273–282
Establish this local claim before using it. It is not an additional assumption.
- L273
have hQ_append : PolynomialEquivalent(q1b,q1c,K1,x18,x19,M + S K0)Definitions: PolynomialEquivalent - L274
specialize prime_field_polynomial_convolution_right_append_equivalent (p) - L275
specialize prime_field_polynomial_convolution_right_append_equivalent (bb) - L276
specialize prime_field_polynomial_convolution_right_append_equivalent (bc) - L277
specialize prime_field_polynomial_convolution_right_append_equivalent (M) - L278
specialize prime_field_polynomial_convolution_right_append_equivalent (cb) - L279
specialize prime_field_polynomial_convolution_right_append_equivalent (cc) - L280
specialize prime_field_polynomial_convolution_right_append_equivalent (J) - L281
specialize prime_field_polynomial_convolution_right_append_equivalent (c) - L282
specialize prime_field_polynomial_convolution_right_append_equivalent (db)
45Use earlier factsL283–292
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L283
specialize prime_field_polynomial_convolution_right_append_equivalent (dc) - L284
specialize prime_field_polynomial_convolution_right_append_equivalent (q0b) - L285
specialize prime_field_polynomial_convolution_right_append_equivalent (q0c) - L286
specialize prime_field_polynomial_convolution_right_append_equivalent (K0) - L287
specialize prime_field_polynomial_convolution_right_append_equivalent (q1b) - L288
specialize prime_field_polynomial_convolution_right_append_equivalent (q1c) - L289
specialize prime_field_polynomial_convolution_right_append_equivalent (K1) - L290
specialize prime_field_polynomial_convolution_right_append_equivalent (x10) - L291
specialize prime_field_polynomial_convolution_right_append_equivalent (x11) - L292
specialize prime_field_polynomial_convolution_right_append_equivalent (x12)
46Use earlier factsL293–302
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L293
specialize prime_field_polynomial_convolution_right_append_equivalent (x13) - L294
specialize prime_field_polynomial_convolution_right_append_equivalent (x14) - L295
specialize prime_field_polynomial_convolution_right_append_equivalent (x15) - L296
specialize prime_field_polynomial_convolution_right_append_equivalent (x16) - L297
specialize prime_field_polynomial_convolution_right_append_equivalent (x17) - L298
specialize prime_field_polynomial_convolution_right_append_equivalent (x18) - L299
specialize prime_field_polynomial_convolution_right_append_equivalent (x19) - L300
apply prime_field_polynomial_convolution_right_append_equivalent - L301
exact hp - L302
exact hprefix
47Use earlier factsL303–310
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L303
exact hlast - L304
exact hQ0 - L305
exact hQ1 - L306
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - L307
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - L308
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - L309
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - L310
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
48Establish hS_transportL311–320
Establish this local claim before using it. It is not an additional assumption.
- L311
have hS_transport : PolynomialEquivalent(s1b,s1c,V1,x21,x22,x20)Definitions: PolynomialEquivalent - L312
specialize prime_field_polynomial_convolution_equivalent_congruent_right (p) - L313
specialize prime_field_polynomial_convolution_equivalent_congruent_right (ab) - L314
specialize prime_field_polynomial_convolution_equivalent_congruent_right (ac) - L315
specialize prime_field_polynomial_convolution_equivalent_congruent_right (L) - L316
specialize prime_field_polynomial_convolution_equivalent_congruent_right (q1b) - L317
specialize prime_field_polynomial_convolution_equivalent_congruent_right (q1c) - L318
specialize prime_field_polynomial_convolution_equivalent_congruent_right (K1) - L319
specialize prime_field_polynomial_convolution_equivalent_congruent_right (s1b) - L320
specialize prime_field_polynomial_convolution_equivalent_congruent_right (s1c)
49Use earlier factsL321–330
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L321
specialize prime_field_polynomial_convolution_equivalent_congruent_right (V1) - L322
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x18) - L323
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x19) - L324
specialize prime_field_polynomial_convolution_equivalent_congruent_right (M+S K0) - L325
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x21) - L326
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x22) - L327
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x20) - L328
apply prime_field_polynomial_convolution_equivalent_congruent_right - L329
exact hp0 - L330
exact hQ_append
50Use earlier factsL331–340
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L331
exact hS1 - L332
exact hAZ_witness_witness - L333
specialize prime_field_polynomial_equivalent_transitive (s1b) - L334
specialize prime_field_polynomial_equivalent_transitive (s1c) - L335
specialize prime_field_polynomial_equivalent_transitive (V1) - L336
specialize prime_field_polynomial_equivalent_transitive (x21) - L337
specialize prime_field_polynomial_equivalent_transitive (x22) - L338
specialize prime_field_polynomial_equivalent_transitive (x20) - L339
specialize prime_field_polynomial_equivalent_transitive (x8) - L340
specialize prime_field_polynomial_equivalent_transitive (x9)
51Use earlier factsL341–344
52Establish hR_totalL345–345
Establish this local claim before using it. It is not an additional assumption.
- L345
have hR_total : PolynomialEquivalent(r1b,r1c,U1,x8,x9,N + S V0)Definitions: PolynomialEquivalent
53Establish hY0alignL346–355
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial shift scale aligned sum exists.
- L346
have hY0align : ∃ ub. ∃ uc. ∃ vb. ∃ vc. ∃ UPb. ∃ UPc. ∃ VPb. ∃ VPc. ∃ zb. ∃ zc. PolynomialShift(r0b,r0c,U0,ub,uc) ∧ (FpPolyScale(p,c,pb,pc,vb,vc,N) ∧ (PolynomialLeftPad(ub,uc,S U0,N,UPb,UPc) ∧ (PolynomialLeftPad(vb,vc,N,S U0,VPb,VPc) ∧ FpPolyAdd(p,UPb,UPc,VPb,VPc,zb,zc,N + S U0))))Definitions: FpPolyAddFpPolyScalePolynomialLeftPadPolynomialShift - L347
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (p) - L348
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (c) - L349
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (pb) - L350
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (pc) - L351
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (N) - L352
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (r0b) - L353
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (r0c) - L354
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (U0) - L355
apply prime_field_polynomial_shift_scale_aligned_sum_exists
54Use earlier factsL356–359
55Separate the logical casesL360–369
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L360
cases hY0align - L361
cases hY0align_witness - L362
cases hY0align_witness_witness - L363
cases hY0align_witness_witness_witness - L364
cases hY0align_witness_witness_witness_witness - L365
cases hY0align_witness_witness_witness_witness_witness - L366
cases hY0align_witness_witness_witness_witness_witness_witness - L367
cases hY0align_witness_witness_witness_witness_witness_witness_witness - L368
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness - L369
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness
56Separate the logical casesL370–373
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L370
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness - L371
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right - L372
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right - L373
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
57Establish hR_appendL374–383
Establish this local claim before using it. It is not an additional assumption.
- L374
have hR_append : PolynomialEquivalent(r1b,r1c,U1,x18,x19,N + S U0)Definitions: PolynomialEquivalent - L375
specialize prime_field_polynomial_convolution_right_append_equivalent (p) - L376
specialize prime_field_polynomial_convolution_right_append_equivalent (pb) - L377
specialize prime_field_polynomial_convolution_right_append_equivalent (pc) - L378
specialize prime_field_polynomial_convolution_right_append_equivalent (N) - L379
specialize prime_field_polynomial_convolution_right_append_equivalent (cb) - L380
specialize prime_field_polynomial_convolution_right_append_equivalent (cc) - L381
specialize prime_field_polynomial_convolution_right_append_equivalent (J) - L382
specialize prime_field_polynomial_convolution_right_append_equivalent (c) - L383
specialize prime_field_polynomial_convolution_right_append_equivalent (db)
58Use earlier factsL384–393
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L384
specialize prime_field_polynomial_convolution_right_append_equivalent (dc) - L385
specialize prime_field_polynomial_convolution_right_append_equivalent (r0b) - L386
specialize prime_field_polynomial_convolution_right_append_equivalent (r0c) - L387
specialize prime_field_polynomial_convolution_right_append_equivalent (U0) - L388
specialize prime_field_polynomial_convolution_right_append_equivalent (r1b) - L389
specialize prime_field_polynomial_convolution_right_append_equivalent (r1c) - L390
specialize prime_field_polynomial_convolution_right_append_equivalent (U1) - L391
specialize prime_field_polynomial_convolution_right_append_equivalent (x10) - L392
specialize prime_field_polynomial_convolution_right_append_equivalent (x11) - L393
specialize prime_field_polynomial_convolution_right_append_equivalent (x12)
59Use earlier factsL394–403
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L394
specialize prime_field_polynomial_convolution_right_append_equivalent (x13) - L395
specialize prime_field_polynomial_convolution_right_append_equivalent (x14) - L396
specialize prime_field_polynomial_convolution_right_append_equivalent (x15) - L397
specialize prime_field_polynomial_convolution_right_append_equivalent (x16) - L398
specialize prime_field_polynomial_convolution_right_append_equivalent (x17) - L399
specialize prime_field_polynomial_convolution_right_append_equivalent (x18) - L400
specialize prime_field_polynomial_convolution_right_append_equivalent (x19) - L401
apply prime_field_polynomial_convolution_right_append_equivalent - L402
exact hp - L403
exact hprefix
60Use earlier factsL404–411
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L404
exact hlast - L405
exact hR0 - L406
exact hR1 - L407
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - L408
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - L409
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - L410
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - L411
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
61Establish haligned_equalL412–421
Establish this local claim before using it. It is not an additional assumption.
- L412
have haligned_equal : PolynomialEquivalent(x18,x19,N + S U0,x8,x9,N + S V0)Definitions: PolynomialEquivalent - L413
specialize prime_field_polynomial_shift_scale_aligned_congruent (p) - L414
specialize prime_field_polynomial_shift_scale_aligned_congruent (c) - L415
specialize prime_field_polynomial_shift_scale_aligned_congruent (pb) - L416
specialize prime_field_polynomial_shift_scale_aligned_congruent (pc) - L417
specialize prime_field_polynomial_shift_scale_aligned_congruent (N) - L418
specialize prime_field_polynomial_shift_scale_aligned_congruent (r0b) - L419
specialize prime_field_polynomial_shift_scale_aligned_congruent (r0c) - L420
specialize prime_field_polynomial_shift_scale_aligned_congruent (U0) - L421
specialize prime_field_polynomial_shift_scale_aligned_congruent (s0b)
62Use earlier factsL422–431
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L422
specialize prime_field_polynomial_shift_scale_aligned_congruent (s0c) - L423
specialize prime_field_polynomial_shift_scale_aligned_congruent (V0) - L424
specialize prime_field_polynomial_shift_scale_aligned_congruent (x10) - L425
specialize prime_field_polynomial_shift_scale_aligned_congruent (x11) - L426
specialize prime_field_polynomial_shift_scale_aligned_congruent (x12) - L427
specialize prime_field_polynomial_shift_scale_aligned_congruent (x13) - L428
specialize prime_field_polynomial_shift_scale_aligned_congruent (x14) - L429
specialize prime_field_polynomial_shift_scale_aligned_congruent (x15) - L430
specialize prime_field_polynomial_shift_scale_aligned_congruent (x16) - L431
specialize prime_field_polynomial_shift_scale_aligned_congruent (x17)
63Use earlier factsL432–441
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L432
specialize prime_field_polynomial_shift_scale_aligned_congruent (x18) - L433
specialize prime_field_polynomial_shift_scale_aligned_congruent (x19) - L434
specialize prime_field_polynomial_shift_scale_aligned_congruent (x) - L435
specialize prime_field_polynomial_shift_scale_aligned_congruent (x1) - L436
specialize prime_field_polynomial_shift_scale_aligned_congruent (x2) - L437
specialize prime_field_polynomial_shift_scale_aligned_congruent (x3) - L438
specialize prime_field_polynomial_shift_scale_aligned_congruent (x4) - L439
specialize prime_field_polynomial_shift_scale_aligned_congruent (x5) - L440
specialize prime_field_polynomial_shift_scale_aligned_congruent (x6) - L441
specialize prime_field_polynomial_shift_scale_aligned_congruent (x7)
64Use earlier factsL442–451
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L442
specialize prime_field_polynomial_shift_scale_aligned_congruent (x8) - L443
specialize prime_field_polynomial_shift_scale_aligned_congruent (x9) - L444
apply prime_field_polynomial_shift_scale_aligned_congruent - L445
exact hp - L446
exact hIH - L447
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - L448
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - L449
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - L450
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - L451
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
65Use earlier factsL452–461
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L452
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - L453
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - L454
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - L455
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - L456
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - L457
specialize prime_field_polynomial_equivalent_transitive (r1b) - L458
specialize prime_field_polynomial_equivalent_transitive (r1c) - L459
specialize prime_field_polynomial_equivalent_transitive (U1) - L460
specialize prime_field_polynomial_equivalent_transitive (x18) - L461
specialize prime_field_polynomial_equivalent_transitive (x19)
66Use earlier factsL462–471
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L462
specialize prime_field_polynomial_equivalent_transitive (N+S U0) - L463
specialize prime_field_polynomial_equivalent_transitive (x8) - L464
specialize prime_field_polynomial_equivalent_transitive (x9) - L465
specialize prime_field_polynomial_equivalent_transitive (N+S V0) - L466
apply prime_field_polynomial_equivalent_transitive - L467
exact hR_append - L468
exact haligned_equal - L469
specialize prime_field_polynomial_equivalent_transitive (r1b) - L470
specialize prime_field_polynomial_equivalent_transitive (r1c) - L471
specialize prime_field_polynomial_equivalent_transitive (U1)
67Use earlier factsL472–481
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L472
specialize prime_field_polynomial_equivalent_transitive (x8) - L473
specialize prime_field_polynomial_equivalent_transitive (x9) - L474
specialize prime_field_polynomial_equivalent_transitive (N+S V0) - L475
specialize prime_field_polynomial_equivalent_transitive (s1b) - L476
specialize prime_field_polynomial_equivalent_transitive (s1c) - L477
specialize prime_field_polynomial_equivalent_transitive (V1) - L478
apply prime_field_polynomial_equivalent_transitive - L479
exact hR_total - L480
specialize prime_field_polynomial_equivalent_symmetric (s1b) - L481
specialize prime_field_polynomial_equivalent_symmetric (s1c)
68Use earlier factsL482–487
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L482
specialize prime_field_polynomial_equivalent_symmetric (V1) - L483
specialize prime_field_polynomial_equivalent_symmetric (x8) - L484
specialize prime_field_polynomial_equivalent_symmetric (x9) - L485
specialize prime_field_polynomial_equivalent_symmetric (N+S V0) - L486
apply prime_field_polynomial_equivalent_symmetric - L487
exact hS_total
Original exact command ledger · 487 lines
- 0001
intro p - 0002
intro ab - 0003
intro ac - 0004
intro L - 0005
intro bb - 0006
intro bc - 0007
intro M - 0008
intro pb - 0009
intro pc - 0010
intro N - 0011
intro cb - 0012
intro cc - 0013
intro J - 0014
intro q0b - 0015
intro q0c - 0016
intro K0 - 0017
intro r0b - 0018
intro r0c - 0019
intro U0 - 0020
intro s0b - 0021
intro s0c - 0022
intro V0 - 0023
intro c - 0024
intro db - 0025
intro dc - 0026
intro q1b - 0027
intro q1c - 0028
intro K1 - 0029
intro r1b - 0030
intro r1c - 0031
intro U1 - 0032
intro s1b - 0033
intro s1c - 0034
intro V1 - 0035
intro hp - 0036
intro hAB - 0037
intro hQ0 - 0038
intro hR0 - 0039
intro hS0 - 0040
intro hIH - 0041
intro hprefix - 0042
intro hlast - 0043
intro hQ1 - 0044
intro hR1 - 0045
intro hS1 - 0046
have hp0 : ~(p=0) - 0047
intro hz - 0048
specialize prime_nonzero (p) - 0049
apply prime_nonzero - 0050
exact hp - 0051
exact hz - 0052
have hABcopy : ((forall fom_index_pfp_append_step_ABleft. (exists fom_gap_pfp_append_step_ABleft_index_bound. fom_gap_pfp_append_step_ABleft_index_bound + S (fom_index_pfp_append_step_ABleft) = L) -> exists fom_value_pfp_append_step_ABleft. ((((exists fom_beta_height_pfp_append_step_ABleft_entry. fom_beta_height_pfp_append_step_ABleft_entry + S (fom_value_pfp_append_step_ABleft) = S ((S (fom_index_pfp_append_step_ABleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_step_ABleft_entry. ab = fom_beta_quotient_pfp_append_step_ABleft_entry * S ((S (fom_index_pfp_append_step_ABleft)) * ac) + (fom_value_pfp_append_step_ABleft))) /\ (exists fom_gap_pfp_append_step_ABleft_value_bound. fom_gap_pfp_append_step_ABleft_value_bound + S (fom_value_pfp_append_step_ABleft) = p))) /\ (((forall fom_index_pfp_append_step_ABright. (exists fom_gap_pfp_append_step_ABright_index_bound. fom_gap_pfp_append_step_ABright_index_bound + S (fom_index_pfp_append_step_ABright) = M) -> exists fom_value_pfp_append_step_ABright. ((((exists fom_beta_height_pfp_append_step_ABright_entry. fom_beta_height_pfp_append_step_ABright_entry + S (fom_value_pfp_append_step_ABright) = S ((S (fom_index_pfp_append_step_ABright)) * bc)) /\ exists fom_beta_quotient_pfp_append_step_ABright_entry. bb = fom_beta_quotient_pfp_append_step_ABright_entry * S ((S (fom_index_pfp_append_step_ABright)) * bc) + (fom_value_pfp_append_step_ABright))) /\ (exists fom_gap_pfp_append_step_ABright_value_bound. fom_gap_pfp_append_step_ABright_value_bound + S (fom_value_pfp_append_step_ABright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_append_step_ABcoefficients. (exists pfa_gap_append_step_ABcoefficientsbound. pfa_gap_append_step_ABcoefficientsbound + S (pfc_index_append_step_ABcoefficients) = (N)) -> exists pfc_value_append_step_ABcoefficients. ((((exists ff_h_pfp_append_step_ABcoefficientsentry. ff_h_pfp_append_step_ABcoefficientsentry + S (pfc_value_append_step_ABcoefficients) = S ((S (pfc_index_append_step_ABcoefficients)) * pc)) /\ exists ff_q_pfp_append_step_ABcoefficientsentry. pb = ff_q_pfp_append_step_ABcoefficientsentry * S ((S (pfc_index_append_step_ABcoefficients)) * pc) + (pfc_value_append_step_ABcoefficients))) /\ ((exists pfc_terms_code_append_step_ABcoefficientscoefficient pfc_terms_scale_append_step_ABcoefficientscoefficient pfc_natural_sum_append_step_ABcoefficientscoefficient. ((forall pfc_index_append_step_ABcoefficientscoefficientdiagonal. (exists pfa_gap_append_step_ABcoefficientscoefficientdiagonalbound. pfa_gap_append_step_ABcoefficientscoefficientdiagonalbound + S (pfc_index_append_step_ABcoefficientscoefficientdiagonal) = (S (pfc_index_append_step_ABcoefficients))) -> exists pfc_value_append_step_ABcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_ABcoefficientscoefficientdiagonalentry. ff_h_pfp_append_step_ABcoefficientscoefficientdiagonalentry + S (pfc_value_append_step_ABcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_ABcoefficientscoefficient)) /\ exists ff_q_pfp_append_step_ABcoefficientscoefficientdiagonalentry. pfc_terms_code_append_step_ABcoefficientscoefficient = ff_q_pfp_append_step_ABcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_ABcoefficientscoefficient) + (pfc_value_append_step_ABcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm pfc_left_append_step_ABcoefficientscoefficientdiagonalterm pfc_right_append_step_ABcoefficientscoefficientdiagonalterm. (((pfc_index_append_step_ABcoefficientscoefficientdiagonal)+pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm=(pfc_index_append_step_ABcoefficients)) /\ ((((((exists pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_ABcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_ABcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_step_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_step_ABcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_ABcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_ABcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_ABcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_append_step_ABcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_append_step_ABcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_ABcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_append_step_ABcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_ABcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_ABcoefficientscoefficientdiagonal)=pfc_left_append_step_ABcoefficientscoefficientdiagonalterm*pfc_right_append_step_ABcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_ABcoefficientscoefficientsum fs_v_pfc_append_step_ABcoefficientscoefficientsum. ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_start. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_start. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_ABcoefficientscoefficient) = S ((S (S (pfc_index_append_step_ABcoefficients))) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_ABcoefficients))) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (pfc_natural_sum_append_step_ABcoefficientscoefficient))) /\ forall fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_ABcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_ABcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps = S (pfc_index_append_step_ABcoefficients)) -> exists fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_ABcoefficientscoefficient)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_ABcoefficientscoefficient = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_ABcoefficientscoefficient) + (fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_ABcoefficientscoefficientsum = fs_q_pfc_append_step_ABcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_ABcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_ABcoefficientscoefficientsum) + (fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_ABcoefficientscoefficientsum_body_steps = fs_r_pfc_append_step_ABcoefficientscoefficientsum_body_steps + fs_a_pfc_append_step_ABcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_ABcoefficientscoefficientresiduebound. pfa_gap_append_step_ABcoefficientscoefficientresiduebound + S (pfc_value_append_step_ABcoefficients) = (p)) /\ ((exists pfa_offset_left_append_step_ABcoefficientscoefficientresiduecongruence pfa_offset_right_append_step_ABcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_ABcoefficientscoefficient) + (p) * pfa_offset_left_append_step_ABcoefficientscoefficientresiduecongruence = (pfc_value_append_step_ABcoefficients) + (p) * pfa_offset_right_append_step_ABcoefficientscoefficientresiduecongruence)))))))))))))))))) - 0053
exact hAB - 0054
cases hABcopy - 0055
cases hABcopy_right - 0056
cases hABcopy_right_right - 0057
have hQ1copy : ((forall fom_index_pfp_append_step_Q1left. (exists fom_gap_pfp_append_step_Q1left_index_bound. fom_gap_pfp_append_step_Q1left_index_bound + S (fom_index_pfp_append_step_Q1left) = M) -> exists fom_value_pfp_append_step_Q1left. ((((exists fom_beta_height_pfp_append_step_Q1left_entry. fom_beta_height_pfp_append_step_Q1left_entry + S (fom_value_pfp_append_step_Q1left) = S ((S (fom_index_pfp_append_step_Q1left)) * bc)) /\ exists fom_beta_quotient_pfp_append_step_Q1left_entry. bb = fom_beta_quotient_pfp_append_step_Q1left_entry * S ((S (fom_index_pfp_append_step_Q1left)) * bc) + (fom_value_pfp_append_step_Q1left))) /\ (exists fom_gap_pfp_append_step_Q1left_value_bound. fom_gap_pfp_append_step_Q1left_value_bound + S (fom_value_pfp_append_step_Q1left) = p))) /\ (((forall fom_index_pfp_append_step_Q1right. (exists fom_gap_pfp_append_step_Q1right_index_bound. fom_gap_pfp_append_step_Q1right_index_bound + S (fom_index_pfp_append_step_Q1right) = S J) -> exists fom_value_pfp_append_step_Q1right. ((((exists fom_beta_height_pfp_append_step_Q1right_entry. fom_beta_height_pfp_append_step_Q1right_entry + S (fom_value_pfp_append_step_Q1right) = S ((S (fom_index_pfp_append_step_Q1right)) * dc)) /\ exists fom_beta_quotient_pfp_append_step_Q1right_entry. db = fom_beta_quotient_pfp_append_step_Q1right_entry * S ((S (fom_index_pfp_append_step_Q1right)) * dc) + (fom_value_pfp_append_step_Q1right))) /\ (exists fom_gap_pfp_append_step_Q1right_value_bound. fom_gap_pfp_append_step_Q1right_value_bound + S (fom_value_pfp_append_step_Q1right) = p))) /\ (((((((M)=0 \/ (S J)=0) /\ (((K1)=0)))) \/ (((~((M)=0)) /\ (((~((S J)=0)) /\ (((M)+(S J)=S (K1)))))))) /\ ((forall pfc_index_append_step_Q1coefficients. (exists pfa_gap_append_step_Q1coefficientsbound. pfa_gap_append_step_Q1coefficientsbound + S (pfc_index_append_step_Q1coefficients) = (K1)) -> exists pfc_value_append_step_Q1coefficients. ((((exists ff_h_pfp_append_step_Q1coefficientsentry. ff_h_pfp_append_step_Q1coefficientsentry + S (pfc_value_append_step_Q1coefficients) = S ((S (pfc_index_append_step_Q1coefficients)) * q1c)) /\ exists ff_q_pfp_append_step_Q1coefficientsentry. q1b = ff_q_pfp_append_step_Q1coefficientsentry * S ((S (pfc_index_append_step_Q1coefficients)) * q1c) + (pfc_value_append_step_Q1coefficients))) /\ ((exists pfc_terms_code_append_step_Q1coefficientscoefficient pfc_terms_scale_append_step_Q1coefficientscoefficient pfc_natural_sum_append_step_Q1coefficientscoefficient. ((forall pfc_index_append_step_Q1coefficientscoefficientdiagonal. (exists pfa_gap_append_step_Q1coefficientscoefficientdiagonalbound. pfa_gap_append_step_Q1coefficientscoefficientdiagonalbound + S (pfc_index_append_step_Q1coefficientscoefficientdiagonal) = (S (pfc_index_append_step_Q1coefficients))) -> exists pfc_value_append_step_Q1coefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_Q1coefficientscoefficientdiagonalentry. ff_h_pfp_append_step_Q1coefficientscoefficientdiagonalentry + S (pfc_value_append_step_Q1coefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q1coefficientscoefficient)) /\ exists ff_q_pfp_append_step_Q1coefficientscoefficientdiagonalentry. pfc_terms_code_append_step_Q1coefficientscoefficient = ff_q_pfp_append_step_Q1coefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_Q1coefficientscoefficient) + (pfc_value_append_step_Q1coefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm pfc_left_append_step_Q1coefficientscoefficientdiagonalterm pfc_right_append_step_Q1coefficientscoefficientdiagonalterm. (((pfc_index_append_step_Q1coefficientscoefficientdiagonal)+pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm=(pfc_index_append_step_Q1coefficients)) /\ ((((((exists pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_Q1coefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_Q1coefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * bc)) /\ exists ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry. bb = ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_Q1coefficientscoefficientdiagonal)) * bc) + (pfc_left_append_step_Q1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_append_step_Q1coefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_Q1coefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_Q1coefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm) = (S J)) /\ ((((exists ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_Q1coefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_append_step_Q1coefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm)) * dc) + (pfc_right_append_step_Q1coefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_Q1coefficientscoefficientdiagonaltermrightoutside+(S J)=(pfc_complement_append_step_Q1coefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_Q1coefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_Q1coefficientscoefficientdiagonal)=pfc_left_append_step_Q1coefficientscoefficientdiagonalterm*pfc_right_append_step_Q1coefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_Q1coefficientscoefficientsum fs_v_pfc_append_step_Q1coefficientscoefficientsum. ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_start. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_start. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_Q1coefficientscoefficient) = S ((S (S (pfc_index_append_step_Q1coefficients))) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_Q1coefficients))) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (pfc_natural_sum_append_step_Q1coefficientscoefficient))) /\ forall fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_Q1coefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_Q1coefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps = S (pfc_index_append_step_Q1coefficients)) -> exists fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q1coefficientscoefficient)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_Q1coefficientscoefficient = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_Q1coefficientscoefficient) + (fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_Q1coefficientscoefficientsum = fs_q_pfc_append_step_Q1coefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_Q1coefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_Q1coefficientscoefficientsum) + (fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_Q1coefficientscoefficientsum_body_steps = fs_r_pfc_append_step_Q1coefficientscoefficientsum_body_steps + fs_a_pfc_append_step_Q1coefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_Q1coefficientscoefficientresiduebound. pfa_gap_append_step_Q1coefficientscoefficientresiduebound + S (pfc_value_append_step_Q1coefficients) = (p)) /\ ((exists pfa_offset_left_append_step_Q1coefficientscoefficientresiduecongruence pfa_offset_right_append_step_Q1coefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_Q1coefficientscoefficient) + (p) * pfa_offset_left_append_step_Q1coefficientscoefficientresiduecongruence = (pfc_value_append_step_Q1coefficients) + (p) * pfa_offset_right_append_step_Q1coefficientscoefficientresiduecongruence)))))))))))))))))) - 0058
exact hQ1 - 0059
cases hQ1copy - 0060
cases hQ1copy_right - 0061
cases hQ1copy_right_right - 0062
have hc : exists pfa_gap_append_step_scalar_bound. pfa_gap_append_step_scalar_bound + S (c) = (p) - 0063
specialize matrix_rank_bounded_prefix_value (db) - 0064
specialize matrix_rank_bounded_prefix_value (dc) - 0065
specialize matrix_rank_bounded_prefix_value (S J) - 0066
specialize matrix_rank_bounded_prefix_value (p) - 0067
specialize matrix_rank_bounded_prefix_value (J) - 0068
specialize matrix_rank_bounded_prefix_value (c) - 0069
apply matrix_rank_bounded_prefix_value - 0070
exact hQ1copy_right_left - 0071
specialize le_refl (S J) - 0072
apply le_refl - 0073
exact hlast - 0074
have hPbound : forall fom_index_pfp_append_step_hPbound. (exists fom_gap_pfp_append_step_hPbound_index_bound. fom_gap_pfp_append_step_hPbound_index_bound + S (fom_index_pfp_append_step_hPbound) = N) -> exists fom_value_pfp_append_step_hPbound. ((((exists fom_beta_height_pfp_append_step_hPbound_entry. fom_beta_height_pfp_append_step_hPbound_entry + S (fom_value_pfp_append_step_hPbound) = S ((S (fom_index_pfp_append_step_hPbound)) * pc)) /\ exists fom_beta_quotient_pfp_append_step_hPbound_entry. pb = fom_beta_quotient_pfp_append_step_hPbound_entry * S ((S (fom_index_pfp_append_step_hPbound)) * pc) + (fom_value_pfp_append_step_hPbound))) /\ (exists fom_gap_pfp_append_step_hPbound_value_bound. fom_gap_pfp_append_step_hPbound_value_bound + S (fom_value_pfp_append_step_hPbound) = p)) - 0075
specialize prime_field_polynomial_convolution_bounded (p) - 0076
specialize prime_field_polynomial_convolution_bounded (ab) - 0077
specialize prime_field_polynomial_convolution_bounded (ac) - 0078
specialize prime_field_polynomial_convolution_bounded (L) - 0079
specialize prime_field_polynomial_convolution_bounded (bb) - 0080
specialize prime_field_polynomial_convolution_bounded (bc) - 0081
specialize prime_field_polynomial_convolution_bounded (M) - 0082
specialize prime_field_polynomial_convolution_bounded (pb) - 0083
specialize prime_field_polynomial_convolution_bounded (pc) - 0084
specialize prime_field_polynomial_convolution_bounded (N) - 0085
apply prime_field_polynomial_convolution_bounded - 0086
exact hAB - 0087
have hQ0bound : forall fom_index_pfp_append_step_hQ0bound. (exists fom_gap_pfp_append_step_hQ0bound_index_bound. fom_gap_pfp_append_step_hQ0bound_index_bound + S (fom_index_pfp_append_step_hQ0bound) = K0) -> exists fom_value_pfp_append_step_hQ0bound. ((((exists fom_beta_height_pfp_append_step_hQ0bound_entry. fom_beta_height_pfp_append_step_hQ0bound_entry + S (fom_value_pfp_append_step_hQ0bound) = S ((S (fom_index_pfp_append_step_hQ0bound)) * q0c)) /\ exists fom_beta_quotient_pfp_append_step_hQ0bound_entry. q0b = fom_beta_quotient_pfp_append_step_hQ0bound_entry * S ((S (fom_index_pfp_append_step_hQ0bound)) * q0c) + (fom_value_pfp_append_step_hQ0bound))) /\ (exists fom_gap_pfp_append_step_hQ0bound_value_bound. fom_gap_pfp_append_step_hQ0bound_value_bound + S (fom_value_pfp_append_step_hQ0bound) = p)) - 0088
specialize prime_field_polynomial_convolution_bounded (p) - 0089
specialize prime_field_polynomial_convolution_bounded (bb) - 0090
specialize prime_field_polynomial_convolution_bounded (bc) - 0091
specialize prime_field_polynomial_convolution_bounded (M) - 0092
specialize prime_field_polynomial_convolution_bounded (cb) - 0093
specialize prime_field_polynomial_convolution_bounded (cc) - 0094
specialize prime_field_polynomial_convolution_bounded (J) - 0095
specialize prime_field_polynomial_convolution_bounded (q0b) - 0096
specialize prime_field_polynomial_convolution_bounded (q0c) - 0097
specialize prime_field_polynomial_convolution_bounded (K0) - 0098
apply prime_field_polynomial_convolution_bounded - 0099
exact hQ0 - 0100
have hR0bound : forall fom_index_pfp_append_step_hR0bound. (exists fom_gap_pfp_append_step_hR0bound_index_bound. fom_gap_pfp_append_step_hR0bound_index_bound + S (fom_index_pfp_append_step_hR0bound) = U0) -> exists fom_value_pfp_append_step_hR0bound. ((((exists fom_beta_height_pfp_append_step_hR0bound_entry. fom_beta_height_pfp_append_step_hR0bound_entry + S (fom_value_pfp_append_step_hR0bound) = S ((S (fom_index_pfp_append_step_hR0bound)) * r0c)) /\ exists fom_beta_quotient_pfp_append_step_hR0bound_entry. r0b = fom_beta_quotient_pfp_append_step_hR0bound_entry * S ((S (fom_index_pfp_append_step_hR0bound)) * r0c) + (fom_value_pfp_append_step_hR0bound))) /\ (exists fom_gap_pfp_append_step_hR0bound_value_bound. fom_gap_pfp_append_step_hR0bound_value_bound + S (fom_value_pfp_append_step_hR0bound) = p)) - 0101
specialize prime_field_polynomial_convolution_bounded (p) - 0102
specialize prime_field_polynomial_convolution_bounded (pb) - 0103
specialize prime_field_polynomial_convolution_bounded (pc) - 0104
specialize prime_field_polynomial_convolution_bounded (N) - 0105
specialize prime_field_polynomial_convolution_bounded (cb) - 0106
specialize prime_field_polynomial_convolution_bounded (cc) - 0107
specialize prime_field_polynomial_convolution_bounded (J) - 0108
specialize prime_field_polynomial_convolution_bounded (r0b) - 0109
specialize prime_field_polynomial_convolution_bounded (r0c) - 0110
specialize prime_field_polynomial_convolution_bounded (U0) - 0111
apply prime_field_polynomial_convolution_bounded - 0112
exact hR0 - 0113
have hS0bound : forall fom_index_pfp_append_step_hS0bound. (exists fom_gap_pfp_append_step_hS0bound_index_bound. fom_gap_pfp_append_step_hS0bound_index_bound + S (fom_index_pfp_append_step_hS0bound) = V0) -> exists fom_value_pfp_append_step_hS0bound. ((((exists fom_beta_height_pfp_append_step_hS0bound_entry. fom_beta_height_pfp_append_step_hS0bound_entry + S (fom_value_pfp_append_step_hS0bound) = S ((S (fom_index_pfp_append_step_hS0bound)) * s0c)) /\ exists fom_beta_quotient_pfp_append_step_hS0bound_entry. s0b = fom_beta_quotient_pfp_append_step_hS0bound_entry * S ((S (fom_index_pfp_append_step_hS0bound)) * s0c) + (fom_value_pfp_append_step_hS0bound))) /\ (exists fom_gap_pfp_append_step_hS0bound_value_bound. fom_gap_pfp_append_step_hS0bound_value_bound + S (fom_value_pfp_append_step_hS0bound) = p)) - 0114
specialize prime_field_polynomial_convolution_bounded (p) - 0115
specialize prime_field_polynomial_convolution_bounded (ab) - 0116
specialize prime_field_polynomial_convolution_bounded (ac) - 0117
specialize prime_field_polynomial_convolution_bounded (L) - 0118
specialize prime_field_polynomial_convolution_bounded (q0b) - 0119
specialize prime_field_polynomial_convolution_bounded (q0c) - 0120
specialize prime_field_polynomial_convolution_bounded (K0) - 0121
specialize prime_field_polynomial_convolution_bounded (s0b) - 0122
specialize prime_field_polynomial_convolution_bounded (s0c) - 0123
specialize prime_field_polynomial_convolution_bounded (V0) - 0124
apply prime_field_polynomial_convolution_bounded - 0125
exact hS0 - 0126
have hYalign : exists ub uc vb vc UPb UPc VPb VPc zb zc. ((((forall mdr_i_pfp_append_step_hYalign_shiftprefix mdr_a_pfp_append_step_hYalign_shiftprefix. (exists mdr_gap_pfp_append_step_hYalign_shiftprefixb. mdr_gap_pfp_append_step_hYalign_shiftprefixb + S (mdr_i_pfp_append_step_hYalign_shiftprefix) = (V0)) -> (((exists ff_h_mdr_pfp_append_step_hYalign_shiftprefixo. ff_h_mdr_pfp_append_step_hYalign_shiftprefixo + S (mdr_a_pfp_append_step_hYalign_shiftprefix) = S ((S (mdr_i_pfp_append_step_hYalign_shiftprefix)) * s0c)) /\ exists ff_q_mdr_pfp_append_step_hYalign_shiftprefixo. s0b = ff_q_mdr_pfp_append_step_hYalign_shiftprefixo * S ((S (mdr_i_pfp_append_step_hYalign_shiftprefix)) * s0c) + (mdr_a_pfp_append_step_hYalign_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_step_hYalign_shiftprefixn. ff_h_mdr_pfp_append_step_hYalign_shiftprefixn + S (mdr_a_pfp_append_step_hYalign_shiftprefix) = S ((S (mdr_i_pfp_append_step_hYalign_shiftprefix)) * uc)) /\ exists ff_q_mdr_pfp_append_step_hYalign_shiftprefixn. ub = ff_q_mdr_pfp_append_step_hYalign_shiftprefixn * S ((S (mdr_i_pfp_append_step_hYalign_shiftprefix)) * uc) + (mdr_a_pfp_append_step_hYalign_shiftprefix)))) /\ ((((exists ff_h_pfp_append_step_hYalign_shiftzero. ff_h_pfp_append_step_hYalign_shiftzero + S (0) = S ((S (V0)) * uc)) /\ exists ff_q_pfp_append_step_hYalign_shiftzero. ub = ff_q_pfp_append_step_hYalign_shiftzero * S ((S (V0)) * uc) + (0)))))) /\ (((((exists pfa_gap_append_step_hYalign_scalescalar. pfa_gap_append_step_hYalign_scalescalar + S (c) = (p)) /\ ((forall pfp_index_append_step_hYalign_scale. (exists pfa_gap_append_step_hYalign_scaleindex. pfa_gap_append_step_hYalign_scaleindex + S (pfp_index_append_step_hYalign_scale) = (N)) -> exists pfp_source_append_step_hYalign_scale pfp_value_append_step_hYalign_scale. ((((exists ff_h_pfp_append_step_hYalign_scalesource. ff_h_pfp_append_step_hYalign_scalesource + S (pfp_source_append_step_hYalign_scale) = S ((S (pfp_index_append_step_hYalign_scale)) * pc)) /\ exists ff_q_pfp_append_step_hYalign_scalesource. pb = ff_q_pfp_append_step_hYalign_scalesource * S ((S (pfp_index_append_step_hYalign_scale)) * pc) + (pfp_source_append_step_hYalign_scale))) /\ (((((exists ff_h_pfp_append_step_hYalign_scaletarget. ff_h_pfp_append_step_hYalign_scaletarget + S (pfp_value_append_step_hYalign_scale) = S ((S (pfp_index_append_step_hYalign_scale)) * vc)) /\ exists ff_q_pfp_append_step_hYalign_scaletarget. vb = ff_q_pfp_append_step_hYalign_scaletarget * S ((S (pfp_index_append_step_hYalign_scale)) * vc) + (pfp_value_append_step_hYalign_scale))) /\ ((((exists pfa_gap_append_step_hYalign_scaleoperationleft. pfa_gap_append_step_hYalign_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_append_step_hYalign_scaleoperationright. pfa_gap_append_step_hYalign_scaleoperationright + S (pfp_source_append_step_hYalign_scale) = (p)) /\ ((((exists pfa_gap_append_step_hYalign_scaleoperationresultbound. pfa_gap_append_step_hYalign_scaleoperationresultbound + S (pfp_value_append_step_hYalign_scale) = (p)) /\ ((exists pfa_offset_left_append_step_hYalign_scaleoperationresultcongruence pfa_offset_right_append_step_hYalign_scaleoperationresultcongruence. ((c) * (pfp_source_append_step_hYalign_scale)) + (p) * pfa_offset_left_append_step_hYalign_scaleoperationresultcongruence = (pfp_value_append_step_hYalign_scale) + (p) * pfa_offset_right_append_step_hYalign_scaleoperationresultcongruence))))))))))))))))) /\ (((((forall pfp_repeat_index_append_step_hYalign_leftzeros. (exists pfa_gap_append_step_hYalign_leftzerosindex. pfa_gap_append_step_hYalign_leftzerosindex + S (pfp_repeat_index_append_step_hYalign_leftzeros) = (N)) -> (((exists ff_h_pfp_append_step_hYalign_leftzerosentry. ff_h_pfp_append_step_hYalign_leftzerosentry + S (0) = S ((S (pfp_repeat_index_append_step_hYalign_leftzeros)) * UPc)) /\ exists ff_q_pfp_append_step_hYalign_leftzerosentry. UPb = ff_q_pfp_append_step_hYalign_leftzerosentry * S ((S (pfp_repeat_index_append_step_hYalign_leftzeros)) * UPc) + (0)))) /\ ((forall pfrep_index_append_step_hYalign_left pfrep_value_append_step_hYalign_left. (exists pfa_gap_append_step_hYalign_leftbound. pfa_gap_append_step_hYalign_leftbound + S (pfrep_index_append_step_hYalign_left) = (S V0)) -> (((exists ff_h_pfp_append_step_hYalign_leftinput. ff_h_pfp_append_step_hYalign_leftinput + S (pfrep_value_append_step_hYalign_left) = S ((S (pfrep_index_append_step_hYalign_left)) * uc)) /\ exists ff_q_pfp_append_step_hYalign_leftinput. ub = ff_q_pfp_append_step_hYalign_leftinput * S ((S (pfrep_index_append_step_hYalign_left)) * uc) + (pfrep_value_append_step_hYalign_left))) -> (((exists ff_h_pfp_append_step_hYalign_leftoutput. ff_h_pfp_append_step_hYalign_leftoutput + S (pfrep_value_append_step_hYalign_left) = S ((S ((N)+pfrep_index_append_step_hYalign_left)) * UPc)) /\ exists ff_q_pfp_append_step_hYalign_leftoutput. UPb = ff_q_pfp_append_step_hYalign_leftoutput * S ((S ((N)+pfrep_index_append_step_hYalign_left)) * UPc) + (pfrep_value_append_step_hYalign_left))))))) /\ (((((forall pfp_repeat_index_append_step_hYalign_rightzeros. (exists pfa_gap_append_step_hYalign_rightzerosindex. pfa_gap_append_step_hYalign_rightzerosindex + S (pfp_repeat_index_append_step_hYalign_rightzeros) = (S V0)) -> (((exists ff_h_pfp_append_step_hYalign_rightzerosentry. ff_h_pfp_append_step_hYalign_rightzerosentry + S (0) = S ((S (pfp_repeat_index_append_step_hYalign_rightzeros)) * VPc)) /\ exists ff_q_pfp_append_step_hYalign_rightzerosentry. VPb = ff_q_pfp_append_step_hYalign_rightzerosentry * S ((S (pfp_repeat_index_append_step_hYalign_rightzeros)) * VPc) + (0)))) /\ ((forall pfrep_index_append_step_hYalign_right pfrep_value_append_step_hYalign_right. (exists pfa_gap_append_step_hYalign_rightbound. pfa_gap_append_step_hYalign_rightbound + S (pfrep_index_append_step_hYalign_right) = (N)) -> (((exists ff_h_pfp_append_step_hYalign_rightinput. ff_h_pfp_append_step_hYalign_rightinput + S (pfrep_value_append_step_hYalign_right) = S ((S (pfrep_index_append_step_hYalign_right)) * vc)) /\ exists ff_q_pfp_append_step_hYalign_rightinput. vb = ff_q_pfp_append_step_hYalign_rightinput * S ((S (pfrep_index_append_step_hYalign_right)) * vc) + (pfrep_value_append_step_hYalign_right))) -> (((exists ff_h_pfp_append_step_hYalign_rightoutput. ff_h_pfp_append_step_hYalign_rightoutput + S (pfrep_value_append_step_hYalign_right) = S ((S ((S V0)+pfrep_index_append_step_hYalign_right)) * VPc)) /\ exists ff_q_pfp_append_step_hYalign_rightoutput. VPb = ff_q_pfp_append_step_hYalign_rightoutput * S ((S ((S V0)+pfrep_index_append_step_hYalign_right)) * VPc) + (pfrep_value_append_step_hYalign_right))))))) /\ ((forall pfp_index_append_step_hYalign_sum. (exists pfa_gap_append_step_hYalign_sumindex. pfa_gap_append_step_hYalign_sumindex + S (pfp_index_append_step_hYalign_sum) = (N+S V0)) -> exists pfp_left_append_step_hYalign_sum pfp_right_append_step_hYalign_sum pfp_value_append_step_hYalign_sum. ((((exists ff_h_pfp_append_step_hYalign_sumleft. ff_h_pfp_append_step_hYalign_sumleft + S (pfp_left_append_step_hYalign_sum) = S ((S (pfp_index_append_step_hYalign_sum)) * UPc)) /\ exists ff_q_pfp_append_step_hYalign_sumleft. UPb = ff_q_pfp_append_step_hYalign_sumleft * S ((S (pfp_index_append_step_hYalign_sum)) * UPc) + (pfp_left_append_step_hYalign_sum))) /\ (((((exists ff_h_pfp_append_step_hYalign_sumright. ff_h_pfp_append_step_hYalign_sumright + S (pfp_right_append_step_hYalign_sum) = S ((S (pfp_index_append_step_hYalign_sum)) * VPc)) /\ exists ff_q_pfp_append_step_hYalign_sumright. VPb = ff_q_pfp_append_step_hYalign_sumright * S ((S (pfp_index_append_step_hYalign_sum)) * VPc) + (pfp_right_append_step_hYalign_sum))) /\ (((((exists ff_h_pfp_append_step_hYalign_sumtarget. ff_h_pfp_append_step_hYalign_sumtarget + S (pfp_value_append_step_hYalign_sum) = S ((S (pfp_index_append_step_hYalign_sum)) * zc)) /\ exists ff_q_pfp_append_step_hYalign_sumtarget. zb = ff_q_pfp_append_step_hYalign_sumtarget * S ((S (pfp_index_append_step_hYalign_sum)) * zc) + (pfp_value_append_step_hYalign_sum))) /\ ((((exists pfa_gap_append_step_hYalign_sumoperationleft. pfa_gap_append_step_hYalign_sumoperationleft + S (pfp_left_append_step_hYalign_sum) = (p)) /\ (((exists pfa_gap_append_step_hYalign_sumoperationright. pfa_gap_append_step_hYalign_sumoperationright + S (pfp_right_append_step_hYalign_sum) = (p)) /\ ((((exists pfa_gap_append_step_hYalign_sumoperationresultbound. pfa_gap_append_step_hYalign_sumoperationresultbound + S (pfp_value_append_step_hYalign_sum) = (p)) /\ ((exists pfa_offset_left_append_step_hYalign_sumoperationresultcongruence pfa_offset_right_append_step_hYalign_sumoperationresultcongruence. ((pfp_left_append_step_hYalign_sum) + (pfp_right_append_step_hYalign_sum)) + (p) * pfa_offset_left_append_step_hYalign_sumoperationresultcongruence = (pfp_value_append_step_hYalign_sum) + (p) * pfa_offset_right_append_step_hYalign_sumoperationresultcongruence)))))))))))))))))))))))) - 0127
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (p) - 0128
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (c) - 0129
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (pb) - 0130
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (pc) - 0131
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (N) - 0132
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (s0b) - 0133
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (s0c) - 0134
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (V0) - 0135
apply prime_field_polynomial_shift_scale_aligned_sum_exists - 0136
exact hp - 0137
exact hc - 0138
exact hPbound - 0139
exact hS0bound - 0140
cases hYalign - 0141
cases hYalign_witness - 0142
cases hYalign_witness_witness - 0143
cases hYalign_witness_witness_witness - 0144
cases hYalign_witness_witness_witness_witness - 0145
cases hYalign_witness_witness_witness_witness_witness - 0146
cases hYalign_witness_witness_witness_witness_witness_witness - 0147
cases hYalign_witness_witness_witness_witness_witness_witness_witness - 0148
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness - 0149
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness - 0150
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness - 0151
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right - 0152
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0153
cases hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - 0154
have hS_total : forall pfrep_power_append_step_S_total pfrep_left_append_step_S_total pfrep_right_append_step_S_total. ((exists pfrep_position_append_step_S_totalfirst. ((pfrep_position_append_step_S_totalfirst+S (pfrep_power_append_step_S_total)=(V1)) /\ ((((exists ff_h_pfp_append_step_S_totalfirstentry. ff_h_pfp_append_step_S_totalfirstentry + S (pfrep_left_append_step_S_total) = S ((S (pfrep_position_append_step_S_totalfirst)) * s1c)) /\ exists ff_q_pfp_append_step_S_totalfirstentry. s1b = ff_q_pfp_append_step_S_totalfirstentry * S ((S (pfrep_position_append_step_S_totalfirst)) * s1c) + (pfrep_left_append_step_S_total)))))) \/ (((exists pfrep_gap_append_step_S_totalfirstoutside. pfrep_gap_append_step_S_totalfirstoutside+(V1)=(pfrep_power_append_step_S_total)) /\ (((pfrep_left_append_step_S_total)=0))))) -> ((exists pfrep_position_append_step_S_totalsecond. ((pfrep_position_append_step_S_totalsecond+S (pfrep_power_append_step_S_total)=(N+S V0)) /\ ((((exists ff_h_pfp_append_step_S_totalsecondentry. ff_h_pfp_append_step_S_totalsecondentry + S (pfrep_right_append_step_S_total) = S ((S (pfrep_position_append_step_S_totalsecond)) * x9)) /\ exists ff_q_pfp_append_step_S_totalsecondentry. x8 = ff_q_pfp_append_step_S_totalsecondentry * S ((S (pfrep_position_append_step_S_totalsecond)) * x9) + (pfrep_right_append_step_S_total)))))) \/ (((exists pfrep_gap_append_step_S_totalsecondoutside. pfrep_gap_append_step_S_totalsecondoutside+(N+S V0)=(pfrep_power_append_step_S_total)) /\ (((pfrep_right_append_step_S_total)=0))))) -> pfrep_left_append_step_S_total=pfrep_right_append_step_S_total - 0155
have hZalign : exists ub uc vb vc UPb UPc VPb VPc zb zc. ((((forall mdr_i_pfp_append_step_hZalign_shiftprefix mdr_a_pfp_append_step_hZalign_shiftprefix. (exists mdr_gap_pfp_append_step_hZalign_shiftprefixb. mdr_gap_pfp_append_step_hZalign_shiftprefixb + S (mdr_i_pfp_append_step_hZalign_shiftprefix) = (K0)) -> (((exists ff_h_mdr_pfp_append_step_hZalign_shiftprefixo. ff_h_mdr_pfp_append_step_hZalign_shiftprefixo + S (mdr_a_pfp_append_step_hZalign_shiftprefix) = S ((S (mdr_i_pfp_append_step_hZalign_shiftprefix)) * q0c)) /\ exists ff_q_mdr_pfp_append_step_hZalign_shiftprefixo. q0b = ff_q_mdr_pfp_append_step_hZalign_shiftprefixo * S ((S (mdr_i_pfp_append_step_hZalign_shiftprefix)) * q0c) + (mdr_a_pfp_append_step_hZalign_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_step_hZalign_shiftprefixn. ff_h_mdr_pfp_append_step_hZalign_shiftprefixn + S (mdr_a_pfp_append_step_hZalign_shiftprefix) = S ((S (mdr_i_pfp_append_step_hZalign_shiftprefix)) * uc)) /\ exists ff_q_mdr_pfp_append_step_hZalign_shiftprefixn. ub = ff_q_mdr_pfp_append_step_hZalign_shiftprefixn * S ((S (mdr_i_pfp_append_step_hZalign_shiftprefix)) * uc) + (mdr_a_pfp_append_step_hZalign_shiftprefix)))) /\ ((((exists ff_h_pfp_append_step_hZalign_shiftzero. ff_h_pfp_append_step_hZalign_shiftzero + S (0) = S ((S (K0)) * uc)) /\ exists ff_q_pfp_append_step_hZalign_shiftzero. ub = ff_q_pfp_append_step_hZalign_shiftzero * S ((S (K0)) * uc) + (0)))))) /\ (((((exists pfa_gap_append_step_hZalign_scalescalar. pfa_gap_append_step_hZalign_scalescalar + S (c) = (p)) /\ ((forall pfp_index_append_step_hZalign_scale. (exists pfa_gap_append_step_hZalign_scaleindex. pfa_gap_append_step_hZalign_scaleindex + S (pfp_index_append_step_hZalign_scale) = (M)) -> exists pfp_source_append_step_hZalign_scale pfp_value_append_step_hZalign_scale. ((((exists ff_h_pfp_append_step_hZalign_scalesource. ff_h_pfp_append_step_hZalign_scalesource + S (pfp_source_append_step_hZalign_scale) = S ((S (pfp_index_append_step_hZalign_scale)) * bc)) /\ exists ff_q_pfp_append_step_hZalign_scalesource. bb = ff_q_pfp_append_step_hZalign_scalesource * S ((S (pfp_index_append_step_hZalign_scale)) * bc) + (pfp_source_append_step_hZalign_scale))) /\ (((((exists ff_h_pfp_append_step_hZalign_scaletarget. ff_h_pfp_append_step_hZalign_scaletarget + S (pfp_value_append_step_hZalign_scale) = S ((S (pfp_index_append_step_hZalign_scale)) * vc)) /\ exists ff_q_pfp_append_step_hZalign_scaletarget. vb = ff_q_pfp_append_step_hZalign_scaletarget * S ((S (pfp_index_append_step_hZalign_scale)) * vc) + (pfp_value_append_step_hZalign_scale))) /\ ((((exists pfa_gap_append_step_hZalign_scaleoperationleft. pfa_gap_append_step_hZalign_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_append_step_hZalign_scaleoperationright. pfa_gap_append_step_hZalign_scaleoperationright + S (pfp_source_append_step_hZalign_scale) = (p)) /\ ((((exists pfa_gap_append_step_hZalign_scaleoperationresultbound. pfa_gap_append_step_hZalign_scaleoperationresultbound + S (pfp_value_append_step_hZalign_scale) = (p)) /\ ((exists pfa_offset_left_append_step_hZalign_scaleoperationresultcongruence pfa_offset_right_append_step_hZalign_scaleoperationresultcongruence. ((c) * (pfp_source_append_step_hZalign_scale)) + (p) * pfa_offset_left_append_step_hZalign_scaleoperationresultcongruence = (pfp_value_append_step_hZalign_scale) + (p) * pfa_offset_right_append_step_hZalign_scaleoperationresultcongruence))))))))))))))))) /\ (((((forall pfp_repeat_index_append_step_hZalign_leftzeros. (exists pfa_gap_append_step_hZalign_leftzerosindex. pfa_gap_append_step_hZalign_leftzerosindex + S (pfp_repeat_index_append_step_hZalign_leftzeros) = (M)) -> (((exists ff_h_pfp_append_step_hZalign_leftzerosentry. ff_h_pfp_append_step_hZalign_leftzerosentry + S (0) = S ((S (pfp_repeat_index_append_step_hZalign_leftzeros)) * UPc)) /\ exists ff_q_pfp_append_step_hZalign_leftzerosentry. UPb = ff_q_pfp_append_step_hZalign_leftzerosentry * S ((S (pfp_repeat_index_append_step_hZalign_leftzeros)) * UPc) + (0)))) /\ ((forall pfrep_index_append_step_hZalign_left pfrep_value_append_step_hZalign_left. (exists pfa_gap_append_step_hZalign_leftbound. pfa_gap_append_step_hZalign_leftbound + S (pfrep_index_append_step_hZalign_left) = (S K0)) -> (((exists ff_h_pfp_append_step_hZalign_leftinput. ff_h_pfp_append_step_hZalign_leftinput + S (pfrep_value_append_step_hZalign_left) = S ((S (pfrep_index_append_step_hZalign_left)) * uc)) /\ exists ff_q_pfp_append_step_hZalign_leftinput. ub = ff_q_pfp_append_step_hZalign_leftinput * S ((S (pfrep_index_append_step_hZalign_left)) * uc) + (pfrep_value_append_step_hZalign_left))) -> (((exists ff_h_pfp_append_step_hZalign_leftoutput. ff_h_pfp_append_step_hZalign_leftoutput + S (pfrep_value_append_step_hZalign_left) = S ((S ((M)+pfrep_index_append_step_hZalign_left)) * UPc)) /\ exists ff_q_pfp_append_step_hZalign_leftoutput. UPb = ff_q_pfp_append_step_hZalign_leftoutput * S ((S ((M)+pfrep_index_append_step_hZalign_left)) * UPc) + (pfrep_value_append_step_hZalign_left))))))) /\ (((((forall pfp_repeat_index_append_step_hZalign_rightzeros. (exists pfa_gap_append_step_hZalign_rightzerosindex. pfa_gap_append_step_hZalign_rightzerosindex + S (pfp_repeat_index_append_step_hZalign_rightzeros) = (S K0)) -> (((exists ff_h_pfp_append_step_hZalign_rightzerosentry. ff_h_pfp_append_step_hZalign_rightzerosentry + S (0) = S ((S (pfp_repeat_index_append_step_hZalign_rightzeros)) * VPc)) /\ exists ff_q_pfp_append_step_hZalign_rightzerosentry. VPb = ff_q_pfp_append_step_hZalign_rightzerosentry * S ((S (pfp_repeat_index_append_step_hZalign_rightzeros)) * VPc) + (0)))) /\ ((forall pfrep_index_append_step_hZalign_right pfrep_value_append_step_hZalign_right. (exists pfa_gap_append_step_hZalign_rightbound. pfa_gap_append_step_hZalign_rightbound + S (pfrep_index_append_step_hZalign_right) = (M)) -> (((exists ff_h_pfp_append_step_hZalign_rightinput. ff_h_pfp_append_step_hZalign_rightinput + S (pfrep_value_append_step_hZalign_right) = S ((S (pfrep_index_append_step_hZalign_right)) * vc)) /\ exists ff_q_pfp_append_step_hZalign_rightinput. vb = ff_q_pfp_append_step_hZalign_rightinput * S ((S (pfrep_index_append_step_hZalign_right)) * vc) + (pfrep_value_append_step_hZalign_right))) -> (((exists ff_h_pfp_append_step_hZalign_rightoutput. ff_h_pfp_append_step_hZalign_rightoutput + S (pfrep_value_append_step_hZalign_right) = S ((S ((S K0)+pfrep_index_append_step_hZalign_right)) * VPc)) /\ exists ff_q_pfp_append_step_hZalign_rightoutput. VPb = ff_q_pfp_append_step_hZalign_rightoutput * S ((S ((S K0)+pfrep_index_append_step_hZalign_right)) * VPc) + (pfrep_value_append_step_hZalign_right))))))) /\ ((forall pfp_index_append_step_hZalign_sum. (exists pfa_gap_append_step_hZalign_sumindex. pfa_gap_append_step_hZalign_sumindex + S (pfp_index_append_step_hZalign_sum) = (M+S K0)) -> exists pfp_left_append_step_hZalign_sum pfp_right_append_step_hZalign_sum pfp_value_append_step_hZalign_sum. ((((exists ff_h_pfp_append_step_hZalign_sumleft. ff_h_pfp_append_step_hZalign_sumleft + S (pfp_left_append_step_hZalign_sum) = S ((S (pfp_index_append_step_hZalign_sum)) * UPc)) /\ exists ff_q_pfp_append_step_hZalign_sumleft. UPb = ff_q_pfp_append_step_hZalign_sumleft * S ((S (pfp_index_append_step_hZalign_sum)) * UPc) + (pfp_left_append_step_hZalign_sum))) /\ (((((exists ff_h_pfp_append_step_hZalign_sumright. ff_h_pfp_append_step_hZalign_sumright + S (pfp_right_append_step_hZalign_sum) = S ((S (pfp_index_append_step_hZalign_sum)) * VPc)) /\ exists ff_q_pfp_append_step_hZalign_sumright. VPb = ff_q_pfp_append_step_hZalign_sumright * S ((S (pfp_index_append_step_hZalign_sum)) * VPc) + (pfp_right_append_step_hZalign_sum))) /\ (((((exists ff_h_pfp_append_step_hZalign_sumtarget. ff_h_pfp_append_step_hZalign_sumtarget + S (pfp_value_append_step_hZalign_sum) = S ((S (pfp_index_append_step_hZalign_sum)) * zc)) /\ exists ff_q_pfp_append_step_hZalign_sumtarget. zb = ff_q_pfp_append_step_hZalign_sumtarget * S ((S (pfp_index_append_step_hZalign_sum)) * zc) + (pfp_value_append_step_hZalign_sum))) /\ ((((exists pfa_gap_append_step_hZalign_sumoperationleft. pfa_gap_append_step_hZalign_sumoperationleft + S (pfp_left_append_step_hZalign_sum) = (p)) /\ (((exists pfa_gap_append_step_hZalign_sumoperationright. pfa_gap_append_step_hZalign_sumoperationright + S (pfp_right_append_step_hZalign_sum) = (p)) /\ ((((exists pfa_gap_append_step_hZalign_sumoperationresultbound. pfa_gap_append_step_hZalign_sumoperationresultbound + S (pfp_value_append_step_hZalign_sum) = (p)) /\ ((exists pfa_offset_left_append_step_hZalign_sumoperationresultcongruence pfa_offset_right_append_step_hZalign_sumoperationresultcongruence. ((pfp_left_append_step_hZalign_sum) + (pfp_right_append_step_hZalign_sum)) + (p) * pfa_offset_left_append_step_hZalign_sumoperationresultcongruence = (pfp_value_append_step_hZalign_sum) + (p) * pfa_offset_right_append_step_hZalign_sumoperationresultcongruence)))))))))))))))))))))))) - 0156
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (p) - 0157
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (c) - 0158
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (bb) - 0159
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (bc) - 0160
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (M) - 0161
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (q0b) - 0162
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (q0c) - 0163
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (K0) - 0164
apply prime_field_polynomial_shift_scale_aligned_sum_exists - 0165
exact hp - 0166
exact hc - 0167
exact hABcopy_right_left - 0168
exact hQ0bound - 0169
cases hZalign - 0170
cases hZalign_witness - 0171
cases hZalign_witness_witness - 0172
cases hZalign_witness_witness_witness - 0173
cases hZalign_witness_witness_witness_witness - 0174
cases hZalign_witness_witness_witness_witness_witness - 0175
cases hZalign_witness_witness_witness_witness_witness_witness - 0176
cases hZalign_witness_witness_witness_witness_witness_witness_witness - 0177
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness - 0178
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness - 0179
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness - 0180
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right - 0181
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0182
cases hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - 0183
have hZbounds : ((forall fom_index_pfp_append_step_Z_left_bound. (exists fom_gap_pfp_append_step_Z_left_bound_index_bound. fom_gap_pfp_append_step_Z_left_bound_index_bound + S (fom_index_pfp_append_step_Z_left_bound) = M+S K0) -> exists fom_value_pfp_append_step_Z_left_bound. ((((exists fom_beta_height_pfp_append_step_Z_left_bound_entry. fom_beta_height_pfp_append_step_Z_left_bound_entry + S (fom_value_pfp_append_step_Z_left_bound) = S ((S (fom_index_pfp_append_step_Z_left_bound)) * x15)) /\ exists fom_beta_quotient_pfp_append_step_Z_left_bound_entry. x14 = fom_beta_quotient_pfp_append_step_Z_left_bound_entry * S ((S (fom_index_pfp_append_step_Z_left_bound)) * x15) + (fom_value_pfp_append_step_Z_left_bound))) /\ (exists fom_gap_pfp_append_step_Z_left_bound_value_bound. fom_gap_pfp_append_step_Z_left_bound_value_bound + S (fom_value_pfp_append_step_Z_left_bound) = p))) /\ (((forall fom_index_pfp_append_step_Z_right_bound. (exists fom_gap_pfp_append_step_Z_right_bound_index_bound. fom_gap_pfp_append_step_Z_right_bound_index_bound + S (fom_index_pfp_append_step_Z_right_bound) = M+S K0) -> exists fom_value_pfp_append_step_Z_right_bound. ((((exists fom_beta_height_pfp_append_step_Z_right_bound_entry. fom_beta_height_pfp_append_step_Z_right_bound_entry + S (fom_value_pfp_append_step_Z_right_bound) = S ((S (fom_index_pfp_append_step_Z_right_bound)) * x17)) /\ exists fom_beta_quotient_pfp_append_step_Z_right_bound_entry. x16 = fom_beta_quotient_pfp_append_step_Z_right_bound_entry * S ((S (fom_index_pfp_append_step_Z_right_bound)) * x17) + (fom_value_pfp_append_step_Z_right_bound))) /\ (exists fom_gap_pfp_append_step_Z_right_bound_value_bound. fom_gap_pfp_append_step_Z_right_bound_value_bound + S (fom_value_pfp_append_step_Z_right_bound) = p))) /\ ((forall fom_index_pfp_append_step_Z_output_bound. (exists fom_gap_pfp_append_step_Z_output_bound_index_bound. fom_gap_pfp_append_step_Z_output_bound_index_bound + S (fom_index_pfp_append_step_Z_output_bound) = M+S K0) -> exists fom_value_pfp_append_step_Z_output_bound. ((((exists fom_beta_height_pfp_append_step_Z_output_bound_entry. fom_beta_height_pfp_append_step_Z_output_bound_entry + S (fom_value_pfp_append_step_Z_output_bound) = S ((S (fom_index_pfp_append_step_Z_output_bound)) * x19)) /\ exists fom_beta_quotient_pfp_append_step_Z_output_bound_entry. x18 = fom_beta_quotient_pfp_append_step_Z_output_bound_entry * S ((S (fom_index_pfp_append_step_Z_output_bound)) * x19) + (fom_value_pfp_append_step_Z_output_bound))) /\ (exists fom_gap_pfp_append_step_Z_output_bound_value_bound. fom_gap_pfp_append_step_Z_output_bound_value_bound + S (fom_value_pfp_append_step_Z_output_bound) = p))))))) - 0184
specialize prime_field_polynomial_add_bounded (p) - 0185
specialize prime_field_polynomial_add_bounded (x14) - 0186
specialize prime_field_polynomial_add_bounded (x15) - 0187
specialize prime_field_polynomial_add_bounded (x16) - 0188
specialize prime_field_polynomial_add_bounded (x17) - 0189
specialize prime_field_polynomial_add_bounded (x18) - 0190
specialize prime_field_polynomial_add_bounded (x19) - 0191
specialize prime_field_polynomial_add_bounded (M+S K0) - 0192
apply prime_field_polynomial_add_bounded - 0193
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0194
cases hZbounds - 0195
cases hZbounds_right - 0196
have hZlength : exists W. (((((L)=0 \/ (M+S K0)=0) /\ (((W)=0)))) \/ (((~((L)=0)) /\ (((~((M+S K0)=0)) /\ (((L)+(M+S K0)=S (W)))))))) - 0197
specialize polynomial_product_length_exists (L) - 0198
specialize polynomial_product_length_exists (M+S K0) - 0199
apply polynomial_product_length_exists - 0200
cases hZlength - 0201
have hAZ : exists mb mc. ((forall fom_index_pfp_append_step_AZleft. (exists fom_gap_pfp_append_step_AZleft_index_bound. fom_gap_pfp_append_step_AZleft_index_bound + S (fom_index_pfp_append_step_AZleft) = L) -> exists fom_value_pfp_append_step_AZleft. ((((exists fom_beta_height_pfp_append_step_AZleft_entry. fom_beta_height_pfp_append_step_AZleft_entry + S (fom_value_pfp_append_step_AZleft) = S ((S (fom_index_pfp_append_step_AZleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_step_AZleft_entry. ab = fom_beta_quotient_pfp_append_step_AZleft_entry * S ((S (fom_index_pfp_append_step_AZleft)) * ac) + (fom_value_pfp_append_step_AZleft))) /\ (exists fom_gap_pfp_append_step_AZleft_value_bound. fom_gap_pfp_append_step_AZleft_value_bound + S (fom_value_pfp_append_step_AZleft) = p))) /\ (((forall fom_index_pfp_append_step_AZright. (exists fom_gap_pfp_append_step_AZright_index_bound. fom_gap_pfp_append_step_AZright_index_bound + S (fom_index_pfp_append_step_AZright) = M+S K0) -> exists fom_value_pfp_append_step_AZright. ((((exists fom_beta_height_pfp_append_step_AZright_entry. fom_beta_height_pfp_append_step_AZright_entry + S (fom_value_pfp_append_step_AZright) = S ((S (fom_index_pfp_append_step_AZright)) * x19)) /\ exists fom_beta_quotient_pfp_append_step_AZright_entry. x18 = fom_beta_quotient_pfp_append_step_AZright_entry * S ((S (fom_index_pfp_append_step_AZright)) * x19) + (fom_value_pfp_append_step_AZright))) /\ (exists fom_gap_pfp_append_step_AZright_value_bound. fom_gap_pfp_append_step_AZright_value_bound + S (fom_value_pfp_append_step_AZright) = p))) /\ (((((((L)=0 \/ (M+S K0)=0) /\ (((x20)=0)))) \/ (((~((L)=0)) /\ (((~((M+S K0)=0)) /\ (((L)+(M+S K0)=S (x20)))))))) /\ ((forall pfc_index_append_step_AZcoefficients. (exists pfa_gap_append_step_AZcoefficientsbound. pfa_gap_append_step_AZcoefficientsbound + S (pfc_index_append_step_AZcoefficients) = (x20)) -> exists pfc_value_append_step_AZcoefficients. ((((exists ff_h_pfp_append_step_AZcoefficientsentry. ff_h_pfp_append_step_AZcoefficientsentry + S (pfc_value_append_step_AZcoefficients) = S ((S (pfc_index_append_step_AZcoefficients)) * mc)) /\ exists ff_q_pfp_append_step_AZcoefficientsentry. mb = ff_q_pfp_append_step_AZcoefficientsentry * S ((S (pfc_index_append_step_AZcoefficients)) * mc) + (pfc_value_append_step_AZcoefficients))) /\ ((exists pfc_terms_code_append_step_AZcoefficientscoefficient pfc_terms_scale_append_step_AZcoefficientscoefficient pfc_natural_sum_append_step_AZcoefficientscoefficient. ((forall pfc_index_append_step_AZcoefficientscoefficientdiagonal. (exists pfa_gap_append_step_AZcoefficientscoefficientdiagonalbound. pfa_gap_append_step_AZcoefficientscoefficientdiagonalbound + S (pfc_index_append_step_AZcoefficientscoefficientdiagonal) = (S (pfc_index_append_step_AZcoefficients))) -> exists pfc_value_append_step_AZcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_step_AZcoefficientscoefficientdiagonalentry. ff_h_pfp_append_step_AZcoefficientscoefficientdiagonalentry + S (pfc_value_append_step_AZcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_step_AZcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_AZcoefficientscoefficient)) /\ exists ff_q_pfp_append_step_AZcoefficientscoefficientdiagonalentry. pfc_terms_code_append_step_AZcoefficientscoefficient = ff_q_pfp_append_step_AZcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_step_AZcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_step_AZcoefficientscoefficient) + (pfc_value_append_step_AZcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_step_AZcoefficientscoefficientdiagonalterm pfc_left_append_step_AZcoefficientscoefficientdiagonalterm pfc_right_append_step_AZcoefficientscoefficientdiagonalterm. (((pfc_index_append_step_AZcoefficientscoefficientdiagonal)+pfc_complement_append_step_AZcoefficientscoefficientdiagonalterm=(pfc_index_append_step_AZcoefficients)) /\ ((((((exists pfa_gap_append_step_AZcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_step_AZcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_step_AZcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_step_AZcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_step_AZcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_step_AZcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_step_AZcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_step_AZcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_step_AZcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_step_AZcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_step_AZcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_AZcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_step_AZcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_step_AZcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_step_AZcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_step_AZcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_step_AZcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_step_AZcoefficientscoefficientdiagonalterm) = (M+S K0)) /\ ((((exists ff_h_pfp_append_step_AZcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_step_AZcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_step_AZcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_step_AZcoefficientscoefficientdiagonalterm)) * x19)) /\ exists ff_q_pfp_append_step_AZcoefficientscoefficientdiagonaltermrightentry. x18 = ff_q_pfp_append_step_AZcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_step_AZcoefficientscoefficientdiagonalterm)) * x19) + (pfc_right_append_step_AZcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_step_AZcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_step_AZcoefficientscoefficientdiagonaltermrightoutside+(M+S K0)=(pfc_complement_append_step_AZcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_step_AZcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_step_AZcoefficientscoefficientdiagonal)=pfc_left_append_step_AZcoefficientscoefficientdiagonalterm*pfc_right_append_step_AZcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_step_AZcoefficientscoefficientsum fs_v_pfc_append_step_AZcoefficientscoefficientsum. ((((exists fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_start. fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_step_AZcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_start. fs_u_pfc_append_step_AZcoefficientscoefficientsum = fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_step_AZcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_step_AZcoefficientscoefficient) = S ((S (S (pfc_index_append_step_AZcoefficients))) * fs_v_pfc_append_step_AZcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_step_AZcoefficientscoefficientsum = fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_step_AZcoefficients))) * fs_v_pfc_append_step_AZcoefficientscoefficientsum) + (pfc_natural_sum_append_step_AZcoefficientscoefficient))) /\ forall fs_i_pfc_append_step_AZcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_step_AZcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_step_AZcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_step_AZcoefficientscoefficientsum_body_steps = S (pfc_index_append_step_AZcoefficients)) -> exists fs_a_pfc_append_step_AZcoefficientscoefficientsum_body_steps fs_r_pfc_append_step_AZcoefficientscoefficientsum_body_steps fs_s_pfc_append_step_AZcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_step_AZcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_AZcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_AZcoefficientscoefficient)) /\ exists fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_step_AZcoefficientscoefficient = fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_step_AZcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_step_AZcoefficientscoefficient) + (fs_a_pfc_append_step_AZcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_step_AZcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_step_AZcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_AZcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_step_AZcoefficientscoefficientsum = fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_step_AZcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_AZcoefficientscoefficientsum) + (fs_r_pfc_append_step_AZcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_step_AZcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_step_AZcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_step_AZcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_AZcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_step_AZcoefficientscoefficientsum = fs_q_pfc_append_step_AZcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_step_AZcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_step_AZcoefficientscoefficientsum) + (fs_s_pfc_append_step_AZcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_step_AZcoefficientscoefficientsum_body_steps = fs_r_pfc_append_step_AZcoefficientscoefficientsum_body_steps + fs_a_pfc_append_step_AZcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_step_AZcoefficientscoefficientresiduebound. pfa_gap_append_step_AZcoefficientscoefficientresiduebound + S (pfc_value_append_step_AZcoefficients) = (p)) /\ ((exists pfa_offset_left_append_step_AZcoefficientscoefficientresiduecongruence pfa_offset_right_append_step_AZcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_step_AZcoefficientscoefficient) + (p) * pfa_offset_left_append_step_AZcoefficientscoefficientresiduecongruence = (pfc_value_append_step_AZcoefficients) + (p) * pfa_offset_right_append_step_AZcoefficientscoefficientresiduecongruence)))))))))))))))))) - 0202
specialize prime_field_polynomial_convolution_at_length_exists (p) - 0203
specialize prime_field_polynomial_convolution_at_length_exists (ab) - 0204
specialize prime_field_polynomial_convolution_at_length_exists (ac) - 0205
specialize prime_field_polynomial_convolution_at_length_exists (L) - 0206
specialize prime_field_polynomial_convolution_at_length_exists (x18) - 0207
specialize prime_field_polynomial_convolution_at_length_exists (x19) - 0208
specialize prime_field_polynomial_convolution_at_length_exists (M+S K0) - 0209
specialize prime_field_polynomial_convolution_at_length_exists (x20) - 0210
apply prime_field_polynomial_convolution_at_length_exists - 0211
exact hp0 - 0212
exact hABcopy_left - 0213
exact hZbounds_right_right - 0214
exact hZlength_witness - 0215
cases hAZ - 0216
cases hAZ_witness - 0217
have hhelper_equal : forall pfrep_power_append_step_helper_equal pfrep_left_append_step_helper_equal pfrep_right_append_step_helper_equal. ((exists pfrep_position_append_step_helper_equalfirst. ((pfrep_position_append_step_helper_equalfirst+S (pfrep_power_append_step_helper_equal)=(x20)) /\ ((((exists ff_h_pfp_append_step_helper_equalfirstentry. ff_h_pfp_append_step_helper_equalfirstentry + S (pfrep_left_append_step_helper_equal) = S ((S (pfrep_position_append_step_helper_equalfirst)) * x22)) /\ exists ff_q_pfp_append_step_helper_equalfirstentry. x21 = ff_q_pfp_append_step_helper_equalfirstentry * S ((S (pfrep_position_append_step_helper_equalfirst)) * x22) + (pfrep_left_append_step_helper_equal)))))) \/ (((exists pfrep_gap_append_step_helper_equalfirstoutside. pfrep_gap_append_step_helper_equalfirstoutside+(x20)=(pfrep_power_append_step_helper_equal)) /\ (((pfrep_left_append_step_helper_equal)=0))))) -> ((exists pfrep_position_append_step_helper_equalsecond. ((pfrep_position_append_step_helper_equalsecond+S (pfrep_power_append_step_helper_equal)=(N+S V0)) /\ ((((exists ff_h_pfp_append_step_helper_equalsecondentry. ff_h_pfp_append_step_helper_equalsecondentry + S (pfrep_right_append_step_helper_equal) = S ((S (pfrep_position_append_step_helper_equalsecond)) * x9)) /\ exists ff_q_pfp_append_step_helper_equalsecondentry. x8 = ff_q_pfp_append_step_helper_equalsecondentry * S ((S (pfrep_position_append_step_helper_equalsecond)) * x9) + (pfrep_right_append_step_helper_equal)))))) \/ (((exists pfrep_gap_append_step_helper_equalsecondoutside. pfrep_gap_append_step_helper_equalsecondoutside+(N+S V0)=(pfrep_power_append_step_helper_equal)) /\ (((pfrep_right_append_step_helper_equal)=0))))) -> pfrep_left_append_step_helper_equal=pfrep_right_append_step_helper_equal - 0218
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (p) - 0219
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (c) - 0220
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (ab) - 0221
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (ac) - 0222
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (L) - 0223
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (bb) - 0224
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (bc) - 0225
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (M) - 0226
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (pb) - 0227
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (pc) - 0228
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (N) - 0229
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (q0b) - 0230
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (q0c) - 0231
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (K0) - 0232
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (s0b) - 0233
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (s0c) - 0234
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (V0) - 0235
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x10) - 0236
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x11) - 0237
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x12) - 0238
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x13) - 0239
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x14) - 0240
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x15) - 0241
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x16) - 0242
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x17) - 0243
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x18) - 0244
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x19) - 0245
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x21) - 0246
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x22) - 0247
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x20) - 0248
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x) - 0249
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x1) - 0250
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x2) - 0251
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x3) - 0252
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x4) - 0253
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x5) - 0254
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x6) - 0255
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x7) - 0256
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x8) - 0257
specialize prime_field_polynomial_convolution_shift_scale_aligned_equivalent (x9) - 0258
apply prime_field_polynomial_convolution_shift_scale_aligned_equivalent - 0259
exact hp - 0260
exact hAB - 0261
exact hS0 - 0262
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - 0263
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0264
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0265
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0266
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0267
exact hAZ_witness_witness - 0268
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - 0269
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0270
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0271
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0272
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0273
have hQ_append : forall pfrep_power_append_step_Q_append pfrep_left_append_step_Q_append pfrep_right_append_step_Q_append. ((exists pfrep_position_append_step_Q_appendfirst. ((pfrep_position_append_step_Q_appendfirst+S (pfrep_power_append_step_Q_append)=(K1)) /\ ((((exists ff_h_pfp_append_step_Q_appendfirstentry. ff_h_pfp_append_step_Q_appendfirstentry + S (pfrep_left_append_step_Q_append) = S ((S (pfrep_position_append_step_Q_appendfirst)) * q1c)) /\ exists ff_q_pfp_append_step_Q_appendfirstentry. q1b = ff_q_pfp_append_step_Q_appendfirstentry * S ((S (pfrep_position_append_step_Q_appendfirst)) * q1c) + (pfrep_left_append_step_Q_append)))))) \/ (((exists pfrep_gap_append_step_Q_appendfirstoutside. pfrep_gap_append_step_Q_appendfirstoutside+(K1)=(pfrep_power_append_step_Q_append)) /\ (((pfrep_left_append_step_Q_append)=0))))) -> ((exists pfrep_position_append_step_Q_appendsecond. ((pfrep_position_append_step_Q_appendsecond+S (pfrep_power_append_step_Q_append)=(M+S K0)) /\ ((((exists ff_h_pfp_append_step_Q_appendsecondentry. ff_h_pfp_append_step_Q_appendsecondentry + S (pfrep_right_append_step_Q_append) = S ((S (pfrep_position_append_step_Q_appendsecond)) * x19)) /\ exists ff_q_pfp_append_step_Q_appendsecondentry. x18 = ff_q_pfp_append_step_Q_appendsecondentry * S ((S (pfrep_position_append_step_Q_appendsecond)) * x19) + (pfrep_right_append_step_Q_append)))))) \/ (((exists pfrep_gap_append_step_Q_appendsecondoutside. pfrep_gap_append_step_Q_appendsecondoutside+(M+S K0)=(pfrep_power_append_step_Q_append)) /\ (((pfrep_right_append_step_Q_append)=0))))) -> pfrep_left_append_step_Q_append=pfrep_right_append_step_Q_append - 0274
specialize prime_field_polynomial_convolution_right_append_equivalent (p) - 0275
specialize prime_field_polynomial_convolution_right_append_equivalent (bb) - 0276
specialize prime_field_polynomial_convolution_right_append_equivalent (bc) - 0277
specialize prime_field_polynomial_convolution_right_append_equivalent (M) - 0278
specialize prime_field_polynomial_convolution_right_append_equivalent (cb) - 0279
specialize prime_field_polynomial_convolution_right_append_equivalent (cc) - 0280
specialize prime_field_polynomial_convolution_right_append_equivalent (J) - 0281
specialize prime_field_polynomial_convolution_right_append_equivalent (c) - 0282
specialize prime_field_polynomial_convolution_right_append_equivalent (db) - 0283
specialize prime_field_polynomial_convolution_right_append_equivalent (dc) - 0284
specialize prime_field_polynomial_convolution_right_append_equivalent (q0b) - 0285
specialize prime_field_polynomial_convolution_right_append_equivalent (q0c) - 0286
specialize prime_field_polynomial_convolution_right_append_equivalent (K0) - 0287
specialize prime_field_polynomial_convolution_right_append_equivalent (q1b) - 0288
specialize prime_field_polynomial_convolution_right_append_equivalent (q1c) - 0289
specialize prime_field_polynomial_convolution_right_append_equivalent (K1) - 0290
specialize prime_field_polynomial_convolution_right_append_equivalent (x10) - 0291
specialize prime_field_polynomial_convolution_right_append_equivalent (x11) - 0292
specialize prime_field_polynomial_convolution_right_append_equivalent (x12) - 0293
specialize prime_field_polynomial_convolution_right_append_equivalent (x13) - 0294
specialize prime_field_polynomial_convolution_right_append_equivalent (x14) - 0295
specialize prime_field_polynomial_convolution_right_append_equivalent (x15) - 0296
specialize prime_field_polynomial_convolution_right_append_equivalent (x16) - 0297
specialize prime_field_polynomial_convolution_right_append_equivalent (x17) - 0298
specialize prime_field_polynomial_convolution_right_append_equivalent (x18) - 0299
specialize prime_field_polynomial_convolution_right_append_equivalent (x19) - 0300
apply prime_field_polynomial_convolution_right_append_equivalent - 0301
exact hp - 0302
exact hprefix - 0303
exact hlast - 0304
exact hQ0 - 0305
exact hQ1 - 0306
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - 0307
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0308
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0309
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0310
exact hZalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0311
have hS_transport : forall pfrep_power_append_step_S_transport pfrep_left_append_step_S_transport pfrep_right_append_step_S_transport. ((exists pfrep_position_append_step_S_transportfirst. ((pfrep_position_append_step_S_transportfirst+S (pfrep_power_append_step_S_transport)=(V1)) /\ ((((exists ff_h_pfp_append_step_S_transportfirstentry. ff_h_pfp_append_step_S_transportfirstentry + S (pfrep_left_append_step_S_transport) = S ((S (pfrep_position_append_step_S_transportfirst)) * s1c)) /\ exists ff_q_pfp_append_step_S_transportfirstentry. s1b = ff_q_pfp_append_step_S_transportfirstentry * S ((S (pfrep_position_append_step_S_transportfirst)) * s1c) + (pfrep_left_append_step_S_transport)))))) \/ (((exists pfrep_gap_append_step_S_transportfirstoutside. pfrep_gap_append_step_S_transportfirstoutside+(V1)=(pfrep_power_append_step_S_transport)) /\ (((pfrep_left_append_step_S_transport)=0))))) -> ((exists pfrep_position_append_step_S_transportsecond. ((pfrep_position_append_step_S_transportsecond+S (pfrep_power_append_step_S_transport)=(x20)) /\ ((((exists ff_h_pfp_append_step_S_transportsecondentry. ff_h_pfp_append_step_S_transportsecondentry + S (pfrep_right_append_step_S_transport) = S ((S (pfrep_position_append_step_S_transportsecond)) * x22)) /\ exists ff_q_pfp_append_step_S_transportsecondentry. x21 = ff_q_pfp_append_step_S_transportsecondentry * S ((S (pfrep_position_append_step_S_transportsecond)) * x22) + (pfrep_right_append_step_S_transport)))))) \/ (((exists pfrep_gap_append_step_S_transportsecondoutside. pfrep_gap_append_step_S_transportsecondoutside+(x20)=(pfrep_power_append_step_S_transport)) /\ (((pfrep_right_append_step_S_transport)=0))))) -> pfrep_left_append_step_S_transport=pfrep_right_append_step_S_transport - 0312
specialize prime_field_polynomial_convolution_equivalent_congruent_right (p) - 0313
specialize prime_field_polynomial_convolution_equivalent_congruent_right (ab) - 0314
specialize prime_field_polynomial_convolution_equivalent_congruent_right (ac) - 0315
specialize prime_field_polynomial_convolution_equivalent_congruent_right (L) - 0316
specialize prime_field_polynomial_convolution_equivalent_congruent_right (q1b) - 0317
specialize prime_field_polynomial_convolution_equivalent_congruent_right (q1c) - 0318
specialize prime_field_polynomial_convolution_equivalent_congruent_right (K1) - 0319
specialize prime_field_polynomial_convolution_equivalent_congruent_right (s1b) - 0320
specialize prime_field_polynomial_convolution_equivalent_congruent_right (s1c) - 0321
specialize prime_field_polynomial_convolution_equivalent_congruent_right (V1) - 0322
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x18) - 0323
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x19) - 0324
specialize prime_field_polynomial_convolution_equivalent_congruent_right (M+S K0) - 0325
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x21) - 0326
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x22) - 0327
specialize prime_field_polynomial_convolution_equivalent_congruent_right (x20) - 0328
apply prime_field_polynomial_convolution_equivalent_congruent_right - 0329
exact hp0 - 0330
exact hQ_append - 0331
exact hS1 - 0332
exact hAZ_witness_witness - 0333
specialize prime_field_polynomial_equivalent_transitive (s1b) - 0334
specialize prime_field_polynomial_equivalent_transitive (s1c) - 0335
specialize prime_field_polynomial_equivalent_transitive (V1) - 0336
specialize prime_field_polynomial_equivalent_transitive (x21) - 0337
specialize prime_field_polynomial_equivalent_transitive (x22) - 0338
specialize prime_field_polynomial_equivalent_transitive (x20) - 0339
specialize prime_field_polynomial_equivalent_transitive (x8) - 0340
specialize prime_field_polynomial_equivalent_transitive (x9) - 0341
specialize prime_field_polynomial_equivalent_transitive (N+S V0) - 0342
apply prime_field_polynomial_equivalent_transitive - 0343
exact hS_transport - 0344
exact hhelper_equal - 0345
have hR_total : forall pfrep_power_append_step_R_total pfrep_left_append_step_R_total pfrep_right_append_step_R_total. ((exists pfrep_position_append_step_R_totalfirst. ((pfrep_position_append_step_R_totalfirst+S (pfrep_power_append_step_R_total)=(U1)) /\ ((((exists ff_h_pfp_append_step_R_totalfirstentry. ff_h_pfp_append_step_R_totalfirstentry + S (pfrep_left_append_step_R_total) = S ((S (pfrep_position_append_step_R_totalfirst)) * r1c)) /\ exists ff_q_pfp_append_step_R_totalfirstentry. r1b = ff_q_pfp_append_step_R_totalfirstentry * S ((S (pfrep_position_append_step_R_totalfirst)) * r1c) + (pfrep_left_append_step_R_total)))))) \/ (((exists pfrep_gap_append_step_R_totalfirstoutside. pfrep_gap_append_step_R_totalfirstoutside+(U1)=(pfrep_power_append_step_R_total)) /\ (((pfrep_left_append_step_R_total)=0))))) -> ((exists pfrep_position_append_step_R_totalsecond. ((pfrep_position_append_step_R_totalsecond+S (pfrep_power_append_step_R_total)=(N+S V0)) /\ ((((exists ff_h_pfp_append_step_R_totalsecondentry. ff_h_pfp_append_step_R_totalsecondentry + S (pfrep_right_append_step_R_total) = S ((S (pfrep_position_append_step_R_totalsecond)) * x9)) /\ exists ff_q_pfp_append_step_R_totalsecondentry. x8 = ff_q_pfp_append_step_R_totalsecondentry * S ((S (pfrep_position_append_step_R_totalsecond)) * x9) + (pfrep_right_append_step_R_total)))))) \/ (((exists pfrep_gap_append_step_R_totalsecondoutside. pfrep_gap_append_step_R_totalsecondoutside+(N+S V0)=(pfrep_power_append_step_R_total)) /\ (((pfrep_right_append_step_R_total)=0))))) -> pfrep_left_append_step_R_total=pfrep_right_append_step_R_total - 0346
have hY0align : exists ub uc vb vc UPb UPc VPb VPc zb zc. ((((forall mdr_i_pfp_append_step_hY0align_shiftprefix mdr_a_pfp_append_step_hY0align_shiftprefix. (exists mdr_gap_pfp_append_step_hY0align_shiftprefixb. mdr_gap_pfp_append_step_hY0align_shiftprefixb + S (mdr_i_pfp_append_step_hY0align_shiftprefix) = (U0)) -> (((exists ff_h_mdr_pfp_append_step_hY0align_shiftprefixo. ff_h_mdr_pfp_append_step_hY0align_shiftprefixo + S (mdr_a_pfp_append_step_hY0align_shiftprefix) = S ((S (mdr_i_pfp_append_step_hY0align_shiftprefix)) * r0c)) /\ exists ff_q_mdr_pfp_append_step_hY0align_shiftprefixo. r0b = ff_q_mdr_pfp_append_step_hY0align_shiftprefixo * S ((S (mdr_i_pfp_append_step_hY0align_shiftprefix)) * r0c) + (mdr_a_pfp_append_step_hY0align_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_step_hY0align_shiftprefixn. ff_h_mdr_pfp_append_step_hY0align_shiftprefixn + S (mdr_a_pfp_append_step_hY0align_shiftprefix) = S ((S (mdr_i_pfp_append_step_hY0align_shiftprefix)) * uc)) /\ exists ff_q_mdr_pfp_append_step_hY0align_shiftprefixn. ub = ff_q_mdr_pfp_append_step_hY0align_shiftprefixn * S ((S (mdr_i_pfp_append_step_hY0align_shiftprefix)) * uc) + (mdr_a_pfp_append_step_hY0align_shiftprefix)))) /\ ((((exists ff_h_pfp_append_step_hY0align_shiftzero. ff_h_pfp_append_step_hY0align_shiftzero + S (0) = S ((S (U0)) * uc)) /\ exists ff_q_pfp_append_step_hY0align_shiftzero. ub = ff_q_pfp_append_step_hY0align_shiftzero * S ((S (U0)) * uc) + (0)))))) /\ (((((exists pfa_gap_append_step_hY0align_scalescalar. pfa_gap_append_step_hY0align_scalescalar + S (c) = (p)) /\ ((forall pfp_index_append_step_hY0align_scale. (exists pfa_gap_append_step_hY0align_scaleindex. pfa_gap_append_step_hY0align_scaleindex + S (pfp_index_append_step_hY0align_scale) = (N)) -> exists pfp_source_append_step_hY0align_scale pfp_value_append_step_hY0align_scale. ((((exists ff_h_pfp_append_step_hY0align_scalesource. ff_h_pfp_append_step_hY0align_scalesource + S (pfp_source_append_step_hY0align_scale) = S ((S (pfp_index_append_step_hY0align_scale)) * pc)) /\ exists ff_q_pfp_append_step_hY0align_scalesource. pb = ff_q_pfp_append_step_hY0align_scalesource * S ((S (pfp_index_append_step_hY0align_scale)) * pc) + (pfp_source_append_step_hY0align_scale))) /\ (((((exists ff_h_pfp_append_step_hY0align_scaletarget. ff_h_pfp_append_step_hY0align_scaletarget + S (pfp_value_append_step_hY0align_scale) = S ((S (pfp_index_append_step_hY0align_scale)) * vc)) /\ exists ff_q_pfp_append_step_hY0align_scaletarget. vb = ff_q_pfp_append_step_hY0align_scaletarget * S ((S (pfp_index_append_step_hY0align_scale)) * vc) + (pfp_value_append_step_hY0align_scale))) /\ ((((exists pfa_gap_append_step_hY0align_scaleoperationleft. pfa_gap_append_step_hY0align_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_append_step_hY0align_scaleoperationright. pfa_gap_append_step_hY0align_scaleoperationright + S (pfp_source_append_step_hY0align_scale) = (p)) /\ ((((exists pfa_gap_append_step_hY0align_scaleoperationresultbound. pfa_gap_append_step_hY0align_scaleoperationresultbound + S (pfp_value_append_step_hY0align_scale) = (p)) /\ ((exists pfa_offset_left_append_step_hY0align_scaleoperationresultcongruence pfa_offset_right_append_step_hY0align_scaleoperationresultcongruence. ((c) * (pfp_source_append_step_hY0align_scale)) + (p) * pfa_offset_left_append_step_hY0align_scaleoperationresultcongruence = (pfp_value_append_step_hY0align_scale) + (p) * pfa_offset_right_append_step_hY0align_scaleoperationresultcongruence))))))))))))))))) /\ (((((forall pfp_repeat_index_append_step_hY0align_leftzeros. (exists pfa_gap_append_step_hY0align_leftzerosindex. pfa_gap_append_step_hY0align_leftzerosindex + S (pfp_repeat_index_append_step_hY0align_leftzeros) = (N)) -> (((exists ff_h_pfp_append_step_hY0align_leftzerosentry. ff_h_pfp_append_step_hY0align_leftzerosentry + S (0) = S ((S (pfp_repeat_index_append_step_hY0align_leftzeros)) * UPc)) /\ exists ff_q_pfp_append_step_hY0align_leftzerosentry. UPb = ff_q_pfp_append_step_hY0align_leftzerosentry * S ((S (pfp_repeat_index_append_step_hY0align_leftzeros)) * UPc) + (0)))) /\ ((forall pfrep_index_append_step_hY0align_left pfrep_value_append_step_hY0align_left. (exists pfa_gap_append_step_hY0align_leftbound. pfa_gap_append_step_hY0align_leftbound + S (pfrep_index_append_step_hY0align_left) = (S U0)) -> (((exists ff_h_pfp_append_step_hY0align_leftinput. ff_h_pfp_append_step_hY0align_leftinput + S (pfrep_value_append_step_hY0align_left) = S ((S (pfrep_index_append_step_hY0align_left)) * uc)) /\ exists ff_q_pfp_append_step_hY0align_leftinput. ub = ff_q_pfp_append_step_hY0align_leftinput * S ((S (pfrep_index_append_step_hY0align_left)) * uc) + (pfrep_value_append_step_hY0align_left))) -> (((exists ff_h_pfp_append_step_hY0align_leftoutput. ff_h_pfp_append_step_hY0align_leftoutput + S (pfrep_value_append_step_hY0align_left) = S ((S ((N)+pfrep_index_append_step_hY0align_left)) * UPc)) /\ exists ff_q_pfp_append_step_hY0align_leftoutput. UPb = ff_q_pfp_append_step_hY0align_leftoutput * S ((S ((N)+pfrep_index_append_step_hY0align_left)) * UPc) + (pfrep_value_append_step_hY0align_left))))))) /\ (((((forall pfp_repeat_index_append_step_hY0align_rightzeros. (exists pfa_gap_append_step_hY0align_rightzerosindex. pfa_gap_append_step_hY0align_rightzerosindex + S (pfp_repeat_index_append_step_hY0align_rightzeros) = (S U0)) -> (((exists ff_h_pfp_append_step_hY0align_rightzerosentry. ff_h_pfp_append_step_hY0align_rightzerosentry + S (0) = S ((S (pfp_repeat_index_append_step_hY0align_rightzeros)) * VPc)) /\ exists ff_q_pfp_append_step_hY0align_rightzerosentry. VPb = ff_q_pfp_append_step_hY0align_rightzerosentry * S ((S (pfp_repeat_index_append_step_hY0align_rightzeros)) * VPc) + (0)))) /\ ((forall pfrep_index_append_step_hY0align_right pfrep_value_append_step_hY0align_right. (exists pfa_gap_append_step_hY0align_rightbound. pfa_gap_append_step_hY0align_rightbound + S (pfrep_index_append_step_hY0align_right) = (N)) -> (((exists ff_h_pfp_append_step_hY0align_rightinput. ff_h_pfp_append_step_hY0align_rightinput + S (pfrep_value_append_step_hY0align_right) = S ((S (pfrep_index_append_step_hY0align_right)) * vc)) /\ exists ff_q_pfp_append_step_hY0align_rightinput. vb = ff_q_pfp_append_step_hY0align_rightinput * S ((S (pfrep_index_append_step_hY0align_right)) * vc) + (pfrep_value_append_step_hY0align_right))) -> (((exists ff_h_pfp_append_step_hY0align_rightoutput. ff_h_pfp_append_step_hY0align_rightoutput + S (pfrep_value_append_step_hY0align_right) = S ((S ((S U0)+pfrep_index_append_step_hY0align_right)) * VPc)) /\ exists ff_q_pfp_append_step_hY0align_rightoutput. VPb = ff_q_pfp_append_step_hY0align_rightoutput * S ((S ((S U0)+pfrep_index_append_step_hY0align_right)) * VPc) + (pfrep_value_append_step_hY0align_right))))))) /\ ((forall pfp_index_append_step_hY0align_sum. (exists pfa_gap_append_step_hY0align_sumindex. pfa_gap_append_step_hY0align_sumindex + S (pfp_index_append_step_hY0align_sum) = (N+S U0)) -> exists pfp_left_append_step_hY0align_sum pfp_right_append_step_hY0align_sum pfp_value_append_step_hY0align_sum. ((((exists ff_h_pfp_append_step_hY0align_sumleft. ff_h_pfp_append_step_hY0align_sumleft + S (pfp_left_append_step_hY0align_sum) = S ((S (pfp_index_append_step_hY0align_sum)) * UPc)) /\ exists ff_q_pfp_append_step_hY0align_sumleft. UPb = ff_q_pfp_append_step_hY0align_sumleft * S ((S (pfp_index_append_step_hY0align_sum)) * UPc) + (pfp_left_append_step_hY0align_sum))) /\ (((((exists ff_h_pfp_append_step_hY0align_sumright. ff_h_pfp_append_step_hY0align_sumright + S (pfp_right_append_step_hY0align_sum) = S ((S (pfp_index_append_step_hY0align_sum)) * VPc)) /\ exists ff_q_pfp_append_step_hY0align_sumright. VPb = ff_q_pfp_append_step_hY0align_sumright * S ((S (pfp_index_append_step_hY0align_sum)) * VPc) + (pfp_right_append_step_hY0align_sum))) /\ (((((exists ff_h_pfp_append_step_hY0align_sumtarget. ff_h_pfp_append_step_hY0align_sumtarget + S (pfp_value_append_step_hY0align_sum) = S ((S (pfp_index_append_step_hY0align_sum)) * zc)) /\ exists ff_q_pfp_append_step_hY0align_sumtarget. zb = ff_q_pfp_append_step_hY0align_sumtarget * S ((S (pfp_index_append_step_hY0align_sum)) * zc) + (pfp_value_append_step_hY0align_sum))) /\ ((((exists pfa_gap_append_step_hY0align_sumoperationleft. pfa_gap_append_step_hY0align_sumoperationleft + S (pfp_left_append_step_hY0align_sum) = (p)) /\ (((exists pfa_gap_append_step_hY0align_sumoperationright. pfa_gap_append_step_hY0align_sumoperationright + S (pfp_right_append_step_hY0align_sum) = (p)) /\ ((((exists pfa_gap_append_step_hY0align_sumoperationresultbound. pfa_gap_append_step_hY0align_sumoperationresultbound + S (pfp_value_append_step_hY0align_sum) = (p)) /\ ((exists pfa_offset_left_append_step_hY0align_sumoperationresultcongruence pfa_offset_right_append_step_hY0align_sumoperationresultcongruence. ((pfp_left_append_step_hY0align_sum) + (pfp_right_append_step_hY0align_sum)) + (p) * pfa_offset_left_append_step_hY0align_sumoperationresultcongruence = (pfp_value_append_step_hY0align_sum) + (p) * pfa_offset_right_append_step_hY0align_sumoperationresultcongruence)))))))))))))))))))))))) - 0347
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (p) - 0348
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (c) - 0349
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (pb) - 0350
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (pc) - 0351
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (N) - 0352
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (r0b) - 0353
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (r0c) - 0354
specialize prime_field_polynomial_shift_scale_aligned_sum_exists (U0) - 0355
apply prime_field_polynomial_shift_scale_aligned_sum_exists - 0356
exact hp - 0357
exact hc - 0358
exact hPbound - 0359
exact hR0bound - 0360
cases hY0align - 0361
cases hY0align_witness - 0362
cases hY0align_witness_witness - 0363
cases hY0align_witness_witness_witness - 0364
cases hY0align_witness_witness_witness_witness - 0365
cases hY0align_witness_witness_witness_witness_witness - 0366
cases hY0align_witness_witness_witness_witness_witness_witness - 0367
cases hY0align_witness_witness_witness_witness_witness_witness_witness - 0368
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness - 0369
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness - 0370
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness - 0371
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right - 0372
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0373
cases hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right - 0374
have hR_append : forall pfrep_power_append_step_R_append pfrep_left_append_step_R_append pfrep_right_append_step_R_append. ((exists pfrep_position_append_step_R_appendfirst. ((pfrep_position_append_step_R_appendfirst+S (pfrep_power_append_step_R_append)=(U1)) /\ ((((exists ff_h_pfp_append_step_R_appendfirstentry. ff_h_pfp_append_step_R_appendfirstentry + S (pfrep_left_append_step_R_append) = S ((S (pfrep_position_append_step_R_appendfirst)) * r1c)) /\ exists ff_q_pfp_append_step_R_appendfirstentry. r1b = ff_q_pfp_append_step_R_appendfirstentry * S ((S (pfrep_position_append_step_R_appendfirst)) * r1c) + (pfrep_left_append_step_R_append)))))) \/ (((exists pfrep_gap_append_step_R_appendfirstoutside. pfrep_gap_append_step_R_appendfirstoutside+(U1)=(pfrep_power_append_step_R_append)) /\ (((pfrep_left_append_step_R_append)=0))))) -> ((exists pfrep_position_append_step_R_appendsecond. ((pfrep_position_append_step_R_appendsecond+S (pfrep_power_append_step_R_append)=(N+S U0)) /\ ((((exists ff_h_pfp_append_step_R_appendsecondentry. ff_h_pfp_append_step_R_appendsecondentry + S (pfrep_right_append_step_R_append) = S ((S (pfrep_position_append_step_R_appendsecond)) * x19)) /\ exists ff_q_pfp_append_step_R_appendsecondentry. x18 = ff_q_pfp_append_step_R_appendsecondentry * S ((S (pfrep_position_append_step_R_appendsecond)) * x19) + (pfrep_right_append_step_R_append)))))) \/ (((exists pfrep_gap_append_step_R_appendsecondoutside. pfrep_gap_append_step_R_appendsecondoutside+(N+S U0)=(pfrep_power_append_step_R_append)) /\ (((pfrep_right_append_step_R_append)=0))))) -> pfrep_left_append_step_R_append=pfrep_right_append_step_R_append - 0375
specialize prime_field_polynomial_convolution_right_append_equivalent (p) - 0376
specialize prime_field_polynomial_convolution_right_append_equivalent (pb) - 0377
specialize prime_field_polynomial_convolution_right_append_equivalent (pc) - 0378
specialize prime_field_polynomial_convolution_right_append_equivalent (N) - 0379
specialize prime_field_polynomial_convolution_right_append_equivalent (cb) - 0380
specialize prime_field_polynomial_convolution_right_append_equivalent (cc) - 0381
specialize prime_field_polynomial_convolution_right_append_equivalent (J) - 0382
specialize prime_field_polynomial_convolution_right_append_equivalent (c) - 0383
specialize prime_field_polynomial_convolution_right_append_equivalent (db) - 0384
specialize prime_field_polynomial_convolution_right_append_equivalent (dc) - 0385
specialize prime_field_polynomial_convolution_right_append_equivalent (r0b) - 0386
specialize prime_field_polynomial_convolution_right_append_equivalent (r0c) - 0387
specialize prime_field_polynomial_convolution_right_append_equivalent (U0) - 0388
specialize prime_field_polynomial_convolution_right_append_equivalent (r1b) - 0389
specialize prime_field_polynomial_convolution_right_append_equivalent (r1c) - 0390
specialize prime_field_polynomial_convolution_right_append_equivalent (U1) - 0391
specialize prime_field_polynomial_convolution_right_append_equivalent (x10) - 0392
specialize prime_field_polynomial_convolution_right_append_equivalent (x11) - 0393
specialize prime_field_polynomial_convolution_right_append_equivalent (x12) - 0394
specialize prime_field_polynomial_convolution_right_append_equivalent (x13) - 0395
specialize prime_field_polynomial_convolution_right_append_equivalent (x14) - 0396
specialize prime_field_polynomial_convolution_right_append_equivalent (x15) - 0397
specialize prime_field_polynomial_convolution_right_append_equivalent (x16) - 0398
specialize prime_field_polynomial_convolution_right_append_equivalent (x17) - 0399
specialize prime_field_polynomial_convolution_right_append_equivalent (x18) - 0400
specialize prime_field_polynomial_convolution_right_append_equivalent (x19) - 0401
apply prime_field_polynomial_convolution_right_append_equivalent - 0402
exact hp - 0403
exact hprefix - 0404
exact hlast - 0405
exact hR0 - 0406
exact hR1 - 0407
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - 0408
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0409
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0410
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0411
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0412
have haligned_equal : forall pfrep_power_append_step_aligned_induction pfrep_left_append_step_aligned_induction pfrep_right_append_step_aligned_induction. ((exists pfrep_position_append_step_aligned_inductionfirst. ((pfrep_position_append_step_aligned_inductionfirst+S (pfrep_power_append_step_aligned_induction)=(N+S U0)) /\ ((((exists ff_h_pfp_append_step_aligned_inductionfirstentry. ff_h_pfp_append_step_aligned_inductionfirstentry + S (pfrep_left_append_step_aligned_induction) = S ((S (pfrep_position_append_step_aligned_inductionfirst)) * x19)) /\ exists ff_q_pfp_append_step_aligned_inductionfirstentry. x18 = ff_q_pfp_append_step_aligned_inductionfirstentry * S ((S (pfrep_position_append_step_aligned_inductionfirst)) * x19) + (pfrep_left_append_step_aligned_induction)))))) \/ (((exists pfrep_gap_append_step_aligned_inductionfirstoutside. pfrep_gap_append_step_aligned_inductionfirstoutside+(N+S U0)=(pfrep_power_append_step_aligned_induction)) /\ (((pfrep_left_append_step_aligned_induction)=0))))) -> ((exists pfrep_position_append_step_aligned_inductionsecond. ((pfrep_position_append_step_aligned_inductionsecond+S (pfrep_power_append_step_aligned_induction)=(N+S V0)) /\ ((((exists ff_h_pfp_append_step_aligned_inductionsecondentry. ff_h_pfp_append_step_aligned_inductionsecondentry + S (pfrep_right_append_step_aligned_induction) = S ((S (pfrep_position_append_step_aligned_inductionsecond)) * x9)) /\ exists ff_q_pfp_append_step_aligned_inductionsecondentry. x8 = ff_q_pfp_append_step_aligned_inductionsecondentry * S ((S (pfrep_position_append_step_aligned_inductionsecond)) * x9) + (pfrep_right_append_step_aligned_induction)))))) \/ (((exists pfrep_gap_append_step_aligned_inductionsecondoutside. pfrep_gap_append_step_aligned_inductionsecondoutside+(N+S V0)=(pfrep_power_append_step_aligned_induction)) /\ (((pfrep_right_append_step_aligned_induction)=0))))) -> pfrep_left_append_step_aligned_induction=pfrep_right_append_step_aligned_induction - 0413
specialize prime_field_polynomial_shift_scale_aligned_congruent (p) - 0414
specialize prime_field_polynomial_shift_scale_aligned_congruent (c) - 0415
specialize prime_field_polynomial_shift_scale_aligned_congruent (pb) - 0416
specialize prime_field_polynomial_shift_scale_aligned_congruent (pc) - 0417
specialize prime_field_polynomial_shift_scale_aligned_congruent (N) - 0418
specialize prime_field_polynomial_shift_scale_aligned_congruent (r0b) - 0419
specialize prime_field_polynomial_shift_scale_aligned_congruent (r0c) - 0420
specialize prime_field_polynomial_shift_scale_aligned_congruent (U0) - 0421
specialize prime_field_polynomial_shift_scale_aligned_congruent (s0b) - 0422
specialize prime_field_polynomial_shift_scale_aligned_congruent (s0c) - 0423
specialize prime_field_polynomial_shift_scale_aligned_congruent (V0) - 0424
specialize prime_field_polynomial_shift_scale_aligned_congruent (x10) - 0425
specialize prime_field_polynomial_shift_scale_aligned_congruent (x11) - 0426
specialize prime_field_polynomial_shift_scale_aligned_congruent (x12) - 0427
specialize prime_field_polynomial_shift_scale_aligned_congruent (x13) - 0428
specialize prime_field_polynomial_shift_scale_aligned_congruent (x14) - 0429
specialize prime_field_polynomial_shift_scale_aligned_congruent (x15) - 0430
specialize prime_field_polynomial_shift_scale_aligned_congruent (x16) - 0431
specialize prime_field_polynomial_shift_scale_aligned_congruent (x17) - 0432
specialize prime_field_polynomial_shift_scale_aligned_congruent (x18) - 0433
specialize prime_field_polynomial_shift_scale_aligned_congruent (x19) - 0434
specialize prime_field_polynomial_shift_scale_aligned_congruent (x) - 0435
specialize prime_field_polynomial_shift_scale_aligned_congruent (x1) - 0436
specialize prime_field_polynomial_shift_scale_aligned_congruent (x2) - 0437
specialize prime_field_polynomial_shift_scale_aligned_congruent (x3) - 0438
specialize prime_field_polynomial_shift_scale_aligned_congruent (x4) - 0439
specialize prime_field_polynomial_shift_scale_aligned_congruent (x5) - 0440
specialize prime_field_polynomial_shift_scale_aligned_congruent (x6) - 0441
specialize prime_field_polynomial_shift_scale_aligned_congruent (x7) - 0442
specialize prime_field_polynomial_shift_scale_aligned_congruent (x8) - 0443
specialize prime_field_polynomial_shift_scale_aligned_congruent (x9) - 0444
apply prime_field_polynomial_shift_scale_aligned_congruent - 0445
exact hp - 0446
exact hIH - 0447
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - 0448
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0449
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0450
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0451
exact hY0align_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0452
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - 0453
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0454
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left - 0455
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left - 0456
exact hYalign_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right - 0457
specialize prime_field_polynomial_equivalent_transitive (r1b) - 0458
specialize prime_field_polynomial_equivalent_transitive (r1c) - 0459
specialize prime_field_polynomial_equivalent_transitive (U1) - 0460
specialize prime_field_polynomial_equivalent_transitive (x18) - 0461
specialize prime_field_polynomial_equivalent_transitive (x19) - 0462
specialize prime_field_polynomial_equivalent_transitive (N+S U0) - 0463
specialize prime_field_polynomial_equivalent_transitive (x8) - 0464
specialize prime_field_polynomial_equivalent_transitive (x9) - 0465
specialize prime_field_polynomial_equivalent_transitive (N+S V0) - 0466
apply prime_field_polynomial_equivalent_transitive - 0467
exact hR_append - 0468
exact haligned_equal - 0469
specialize prime_field_polynomial_equivalent_transitive (r1b) - 0470
specialize prime_field_polynomial_equivalent_transitive (r1c) - 0471
specialize prime_field_polynomial_equivalent_transitive (U1) - 0472
specialize prime_field_polynomial_equivalent_transitive (x8) - 0473
specialize prime_field_polynomial_equivalent_transitive (x9) - 0474
specialize prime_field_polynomial_equivalent_transitive (N+S V0) - 0475
specialize prime_field_polynomial_equivalent_transitive (s1b) - 0476
specialize prime_field_polynomial_equivalent_transitive (s1c) - 0477
specialize prime_field_polynomial_equivalent_transitive (V1) - 0478
apply prime_field_polynomial_equivalent_transitive - 0479
exact hR_total - 0480
specialize prime_field_polynomial_equivalent_symmetric (s1b) - 0481
specialize prime_field_polynomial_equivalent_symmetric (s1c) - 0482
specialize prime_field_polynomial_equivalent_symmetric (V1) - 0483
specialize prime_field_polynomial_equivalent_symmetric (x8) - 0484
specialize prime_field_polynomial_equivalent_symmetric (x9) - 0485
specialize prime_field_polynomial_equivalent_symmetric (N+S V0) - 0486
apply prime_field_polynomial_equivalent_symmetric - 0487
exact hS_total