prime_field_polynomial_quotient_step_recode

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc M qb qc QB QC i q. (forall mdr_i_pfp_division_step_recode mdr_a_pfp_division_step_recode. (exists mdr_gap_pfp_division_step_recodeb. mdr_gap_pfp_division_step_recodeb + S (mdr_i_pfp_division_step_recode) = (i)) -> (((exists ff_h_mdr_pfp_division_step_recodeo. ff_h_mdr_pfp_division_step_recodeo + S (mdr_a_pfp_division_step_recode) = S ((S (mdr_i_pfp_division_step_recode)) * qc)) /\ exists ff_q_mdr_pfp_division_step_recodeo. qb = ff_q_mdr_pfp_division_step_recodeo * S ((S (mdr_i_pfp_division_step_recode)) * qc) + (mdr_a_pfp_division_step_recode))) -> (((exists ff_h_mdr_pfp_division_step_recoden. ff_h_mdr_pfp_division_step_recoden + S (mdr_a_pfp_division_step_recode) = S ((S (mdr_i_pfp_division_step_recode)) * QC)) /\ exists ff_q_mdr_pfp_division_step_recoden. QB = ff_q_mdr_pfp_division_step_recoden * S ((S (mdr_i_pfp_division_step_recode)) * QC) + (mdr_a_pfp_division_step_recode)))) -> (exists pfd_input_division_step_old pfd_previous_division_step_old pfd_difference_division_step_old. ((((exists ff_h_pfp_division_step_oldinput. ff_h_pfp_division_step_oldinput + S (pfd_input_division_step_old) = S ((S (i)) * ac)) /\ exists ff_q_pfp_division_step_oldinput. ab = ff_q_pfp_division_step_oldinput * S ((S (i)) * ac) + (pfd_input_division_step_old))) /\ (((exists pfc_terms_code_division_step_oldprevious pfc_terms_scale_division_step_oldprevious pfc_natural_sum_division_step_oldprevious. ((forall pfc_index_division_step_oldpreviousdiagonal. (exists pfa_gap_division_step_oldpreviousdiagonalbound. pfa_gap_division_step_oldpreviousdiagonalbound + S (pfc_index_division_step_oldpreviousdiagonal) = (S (i))) -> exists pfc_value_division_step_oldpreviousdiagonal. ((((exists ff_h_pfp_division_step_oldpreviousdiagonalentry. ff_h_pfp_division_step_oldpreviousdiagonalentry + S (pfc_value_division_step_oldpreviousdiagonal) = S ((S (pfc_index_division_step_oldpreviousdiagonal)) * pfc_terms_scale_division_step_oldprevious)) /\ exists ff_q_pfp_division_step_oldpreviousdiagonalentry. pfc_terms_code_division_step_oldprevious = ff_q_pfp_division_step_oldpreviousdiagonalentry * S ((S (pfc_index_division_step_oldpreviousdiagonal)) * pfc_terms_scale_division_step_oldprevious) + (pfc_value_division_step_oldpreviousdiagonal))) /\ ((exists pfc_complement_division_step_oldpreviousdiagonalterm pfc_left_division_step_oldpreviousdiagonalterm pfc_right_division_step_oldpreviousdiagonalterm. (((pfc_index_division_step_oldpreviousdiagonal)+pfc_complement_division_step_oldpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_division_step_oldpreviousdiagonaltermleftinside. pfa_gap_division_step_oldpreviousdiagonaltermleftinside + S (pfc_index_division_step_oldpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_division_step_oldpreviousdiagonaltermleftentry. ff_h_pfp_division_step_oldpreviousdiagonaltermleftentry + S (pfc_left_division_step_oldpreviousdiagonalterm) = S ((S (pfc_index_division_step_oldpreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_step_oldpreviousdiagonaltermleftentry. qb = ff_q_pfp_division_step_oldpreviousdiagonaltermleftentry * S ((S (pfc_index_division_step_oldpreviousdiagonal)) * qc) + (pfc_left_division_step_oldpreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_step_oldpreviousdiagonaltermleftoutside. pfc_gap_division_step_oldpreviousdiagonaltermleftoutside+(i)=(pfc_index_division_step_oldpreviousdiagonal)) /\ (((pfc_left_division_step_oldpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_step_oldpreviousdiagonaltermrightinside. pfa_gap_division_step_oldpreviousdiagonaltermrightinside + S (pfc_complement_division_step_oldpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_step_oldpreviousdiagonaltermrightentry. ff_h_pfp_division_step_oldpreviousdiagonaltermrightentry + S (pfc_right_division_step_oldpreviousdiagonalterm) = S ((S (pfc_complement_division_step_oldpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_step_oldpreviousdiagonaltermrightentry. bb = ff_q_pfp_division_step_oldpreviousdiagonaltermrightentry * S ((S (pfc_complement_division_step_oldpreviousdiagonalterm)) * bc) + (pfc_right_division_step_oldpreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_step_oldpreviousdiagonaltermrightoutside. pfc_gap_division_step_oldpreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_step_oldpreviousdiagonalterm)) /\ (((pfc_right_division_step_oldpreviousdiagonalterm)=0))))) /\ (((pfc_value_division_step_oldpreviousdiagonal)=pfc_left_division_step_oldpreviousdiagonalterm*pfc_right_division_step_oldpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_step_oldprevioussum fs_v_pfc_division_step_oldprevioussum. ((((exists fs_h_pfc_division_step_oldprevioussum_body_start. fs_h_pfc_division_step_oldprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_step_oldprevioussum)) /\ exists fs_q_pfc_division_step_oldprevioussum_body_start. fs_u_pfc_division_step_oldprevioussum = fs_q_pfc_division_step_oldprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_step_oldprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_step_oldprevioussum_body_terminal. fs_h_pfc_division_step_oldprevioussum_body_terminal + S (pfc_natural_sum_division_step_oldprevious) = S ((S (S (i))) * fs_v_pfc_division_step_oldprevioussum)) /\ exists fs_q_pfc_division_step_oldprevioussum_body_terminal. fs_u_pfc_division_step_oldprevioussum = fs_q_pfc_division_step_oldprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_division_step_oldprevioussum) + (pfc_natural_sum_division_step_oldprevious))) /\ forall fs_i_pfc_division_step_oldprevioussum_body_steps. (exists fs_lt_pfc_division_step_oldprevioussum_body_steps_bound. fs_lt_pfc_division_step_oldprevioussum_body_steps_bound + S fs_i_pfc_division_step_oldprevioussum_body_steps = S (i)) -> exists fs_a_pfc_division_step_oldprevioussum_body_steps fs_r_pfc_division_step_oldprevioussum_body_steps fs_s_pfc_division_step_oldprevioussum_body_steps. ((((exists fs_h_pfc_division_step_oldprevioussum_body_steps_summand. fs_h_pfc_division_step_oldprevioussum_body_steps_summand + S (fs_a_pfc_division_step_oldprevioussum_body_steps) = S ((S (fs_i_pfc_division_step_oldprevioussum_body_steps)) * pfc_terms_scale_division_step_oldprevious)) /\ exists fs_q_pfc_division_step_oldprevioussum_body_steps_summand. pfc_terms_code_division_step_oldprevious = fs_q_pfc_division_step_oldprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_step_oldprevioussum_body_steps)) * pfc_terms_scale_division_step_oldprevious) + (fs_a_pfc_division_step_oldprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_step_oldprevioussum_body_steps_partial. fs_h_pfc_division_step_oldprevioussum_body_steps_partial + S (fs_r_pfc_division_step_oldprevioussum_body_steps) = S ((S (fs_i_pfc_division_step_oldprevioussum_body_steps)) * fs_v_pfc_division_step_oldprevioussum)) /\ exists fs_q_pfc_division_step_oldprevioussum_body_steps_partial. fs_u_pfc_division_step_oldprevioussum = fs_q_pfc_division_step_oldprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_step_oldprevioussum_body_steps)) * fs_v_pfc_division_step_oldprevioussum) + (fs_r_pfc_division_step_oldprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_step_oldprevioussum_body_steps_successor. fs_h_pfc_division_step_oldprevioussum_body_steps_successor + S (fs_s_pfc_division_step_oldprevioussum_body_steps) = S ((S (S fs_i_pfc_division_step_oldprevioussum_body_steps)) * fs_v_pfc_division_step_oldprevioussum)) /\ exists fs_q_pfc_division_step_oldprevioussum_body_steps_successor. fs_u_pfc_division_step_oldprevioussum = fs_q_pfc_division_step_oldprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_step_oldprevioussum_body_steps)) * fs_v_pfc_division_step_oldprevioussum) + (fs_s_pfc_division_step_oldprevioussum_body_steps))) /\ fs_s_pfc_division_step_oldprevioussum_body_steps = fs_r_pfc_division_step_oldprevioussum_body_steps + fs_a_pfc_division_step_oldprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_step_oldpreviousresiduebound. pfa_gap_division_step_oldpreviousresiduebound + S (pfd_previous_division_step_old) = (p)) /\ ((exists pfa_offset_left_division_step_oldpreviousresiduecongruence pfa_offset_right_division_step_oldpreviousresiduecongruence. (pfc_natural_sum_division_step_oldprevious) + (p) * pfa_offset_left_division_step_oldpreviousresiduecongruence = (pfd_previous_division_step_old) + (p) * pfa_offset_right_division_step_oldpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_step_oldsubtractleft. pfa_gap_division_step_oldsubtractleft + S (pfd_previous_division_step_old) = (p)) /\ (((exists pfa_gap_division_step_oldsubtractright. pfa_gap_division_step_oldsubtractright + S (pfd_difference_division_step_old) = (p)) /\ ((((exists pfa_gap_division_step_oldsubtractresultbound. pfa_gap_division_step_oldsubtractresultbound + S (pfd_input_division_step_old) = (p)) /\ ((exists pfa_offset_left_division_step_oldsubtractresultcongruence pfa_offset_right_division_step_oldsubtractresultcongruence. ((pfd_previous_division_step_old) + (pfd_difference_division_step_old)) + (p) * pfa_offset_left_division_step_oldsubtractresultcongruence = (pfd_input_division_step_old) + (p) * pfa_offset_right_division_step_oldsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_step_oldmultiplyleft. pfa_gap_division_step_oldmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_step_oldmultiplyright. pfa_gap_division_step_oldmultiplyright + S (pfd_difference_division_step_old) = (p)) /\ ((((exists pfa_gap_division_step_oldmultiplyresultbound. pfa_gap_division_step_oldmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_division_step_oldmultiplyresultcongruence pfa_offset_right_division_step_oldmultiplyresultcongruence. ((k) * (pfd_difference_division_step_old)) + (p) * pfa_offset_left_division_step_oldmultiplyresultcongruence = (q) + (p) * pfa_offset_right_division_step_oldmultiplyresultcongruence)))))))))))))))) -> (exists pfd_input_division_step_new pfd_previous_division_step_new pfd_difference_division_step_new. ((((exists ff_h_pfp_division_step_newinput. ff_h_pfp_division_step_newinput + S (pfd_input_division_step_new) = S ((S (i)) * ac)) /\ exists ff_q_pfp_division_step_newinput. ab = ff_q_pfp_division_step_newinput * S ((S (i)) * ac) + (pfd_input_division_step_new))) /\ (((exists pfc_terms_code_division_step_newprevious pfc_terms_scale_division_step_newprevious pfc_natural_sum_division_step_newprevious. ((forall pfc_index_division_step_newpreviousdiagonal. (exists pfa_gap_division_step_newpreviousdiagonalbound. pfa_gap_division_step_newpreviousdiagonalbound + S (pfc_index_division_step_newpreviousdiagonal) = (S (i))) -> exists pfc_value_division_step_newpreviousdiagonal. ((((exists ff_h_pfp_division_step_newpreviousdiagonalentry. ff_h_pfp_division_step_newpreviousdiagonalentry + S (pfc_value_division_step_newpreviousdiagonal) = S ((S (pfc_index_division_step_newpreviousdiagonal)) * pfc_terms_scale_division_step_newprevious)) /\ exists ff_q_pfp_division_step_newpreviousdiagonalentry. pfc_terms_code_division_step_newprevious = ff_q_pfp_division_step_newpreviousdiagonalentry * S ((S (pfc_index_division_step_newpreviousdiagonal)) * pfc_terms_scale_division_step_newprevious) + (pfc_value_division_step_newpreviousdiagonal))) /\ ((exists pfc_complement_division_step_newpreviousdiagonalterm pfc_left_division_step_newpreviousdiagonalterm pfc_right_division_step_newpreviousdiagonalterm. (((pfc_index_division_step_newpreviousdiagonal)+pfc_complement_division_step_newpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_division_step_newpreviousdiagonaltermleftinside. pfa_gap_division_step_newpreviousdiagonaltermleftinside + S (pfc_index_division_step_newpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_division_step_newpreviousdiagonaltermleftentry. ff_h_pfp_division_step_newpreviousdiagonaltermleftentry + S (pfc_left_division_step_newpreviousdiagonalterm) = S ((S (pfc_index_division_step_newpreviousdiagonal)) * QC)) /\ exists ff_q_pfp_division_step_newpreviousdiagonaltermleftentry. QB = ff_q_pfp_division_step_newpreviousdiagonaltermleftentry * S ((S (pfc_index_division_step_newpreviousdiagonal)) * QC) + (pfc_left_division_step_newpreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_step_newpreviousdiagonaltermleftoutside. pfc_gap_division_step_newpreviousdiagonaltermleftoutside+(i)=(pfc_index_division_step_newpreviousdiagonal)) /\ (((pfc_left_division_step_newpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_step_newpreviousdiagonaltermrightinside. pfa_gap_division_step_newpreviousdiagonaltermrightinside + S (pfc_complement_division_step_newpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_step_newpreviousdiagonaltermrightentry. ff_h_pfp_division_step_newpreviousdiagonaltermrightentry + S (pfc_right_division_step_newpreviousdiagonalterm) = S ((S (pfc_complement_division_step_newpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_step_newpreviousdiagonaltermrightentry. bb = ff_q_pfp_division_step_newpreviousdiagonaltermrightentry * S ((S (pfc_complement_division_step_newpreviousdiagonalterm)) * bc) + (pfc_right_division_step_newpreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_step_newpreviousdiagonaltermrightoutside. pfc_gap_division_step_newpreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_step_newpreviousdiagonalterm)) /\ (((pfc_right_division_step_newpreviousdiagonalterm)=0))))) /\ (((pfc_value_division_step_newpreviousdiagonal)=pfc_left_division_step_newpreviousdiagonalterm*pfc_right_division_step_newpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_step_newprevioussum fs_v_pfc_division_step_newprevioussum. ((((exists fs_h_pfc_division_step_newprevioussum_body_start. fs_h_pfc_division_step_newprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_step_newprevioussum)) /\ exists fs_q_pfc_division_step_newprevioussum_body_start. fs_u_pfc_division_step_newprevioussum = fs_q_pfc_division_step_newprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_step_newprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_step_newprevioussum_body_terminal. fs_h_pfc_division_step_newprevioussum_body_terminal + S (pfc_natural_sum_division_step_newprevious) = S ((S (S (i))) * fs_v_pfc_division_step_newprevioussum)) /\ exists fs_q_pfc_division_step_newprevioussum_body_terminal. fs_u_pfc_division_step_newprevioussum = fs_q_pfc_division_step_newprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_division_step_newprevioussum) + (pfc_natural_sum_division_step_newprevious))) /\ forall fs_i_pfc_division_step_newprevioussum_body_steps. (exists fs_lt_pfc_division_step_newprevioussum_body_steps_bound. fs_lt_pfc_division_step_newprevioussum_body_steps_bound + S fs_i_pfc_division_step_newprevioussum_body_steps = S (i)) -> exists fs_a_pfc_division_step_newprevioussum_body_steps fs_r_pfc_division_step_newprevioussum_body_steps fs_s_pfc_division_step_newprevioussum_body_steps. ((((exists fs_h_pfc_division_step_newprevioussum_body_steps_summand. fs_h_pfc_division_step_newprevioussum_body_steps_summand + S (fs_a_pfc_division_step_newprevioussum_body_steps) = S ((S (fs_i_pfc_division_step_newprevioussum_body_steps)) * pfc_terms_scale_division_step_newprevious)) /\ exists fs_q_pfc_division_step_newprevioussum_body_steps_summand. pfc_terms_code_division_step_newprevious = fs_q_pfc_division_step_newprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_step_newprevioussum_body_steps)) * pfc_terms_scale_division_step_newprevious) + (fs_a_pfc_division_step_newprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_step_newprevioussum_body_steps_partial. fs_h_pfc_division_step_newprevioussum_body_steps_partial + S (fs_r_pfc_division_step_newprevioussum_body_steps) = S ((S (fs_i_pfc_division_step_newprevioussum_body_steps)) * fs_v_pfc_division_step_newprevioussum)) /\ exists fs_q_pfc_division_step_newprevioussum_body_steps_partial. fs_u_pfc_division_step_newprevioussum = fs_q_pfc_division_step_newprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_step_newprevioussum_body_steps)) * fs_v_pfc_division_step_newprevioussum) + (fs_r_pfc_division_step_newprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_step_newprevioussum_body_steps_successor. fs_h_pfc_division_step_newprevioussum_body_steps_successor + S (fs_s_pfc_division_step_newprevioussum_body_steps) = S ((S (S fs_i_pfc_division_step_newprevioussum_body_steps)) * fs_v_pfc_division_step_newprevioussum)) /\ exists fs_q_pfc_division_step_newprevioussum_body_steps_successor. fs_u_pfc_division_step_newprevioussum = fs_q_pfc_division_step_newprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_step_newprevioussum_body_steps)) * fs_v_pfc_division_step_newprevioussum) + (fs_s_pfc_division_step_newprevioussum_body_steps))) /\ fs_s_pfc_division_step_newprevioussum_body_steps = fs_r_pfc_division_step_newprevioussum_body_steps + fs_a_pfc_division_step_newprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_step_newpreviousresiduebound. pfa_gap_division_step_newpreviousresiduebound + S (pfd_previous_division_step_new) = (p)) /\ ((exists pfa_offset_left_division_step_newpreviousresiduecongruence pfa_offset_right_division_step_newpreviousresiduecongruence. (pfc_natural_sum_division_step_newprevious) + (p) * pfa_offset_left_division_step_newpreviousresiduecongruence = (pfd_previous_division_step_new) + (p) * pfa_offset_right_division_step_newpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_step_newsubtractleft. pfa_gap_division_step_newsubtractleft + S (pfd_previous_division_step_new) = (p)) /\ (((exists pfa_gap_division_step_newsubtractright. pfa_gap_division_step_newsubtractright + S (pfd_difference_division_step_new) = (p)) /\ ((((exists pfa_gap_division_step_newsubtractresultbound. pfa_gap_division_step_newsubtractresultbound + S (pfd_input_division_step_new) = (p)) /\ ((exists pfa_offset_left_division_step_newsubtractresultcongruence pfa_offset_right_division_step_newsubtractresultcongruence. ((pfd_previous_division_step_new) + (pfd_difference_division_step_new)) + (p) * pfa_offset_left_division_step_newsubtractresultcongruence = (pfd_input_division_step_new) + (p) * pfa_offset_right_division_step_newsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_step_newmultiplyleft. pfa_gap_division_step_newmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_step_newmultiplyright. pfa_gap_division_step_newmultiplyright + S (pfd_difference_division_step_new) = (p)) /\ ((((exists pfa_gap_division_step_newmultiplyresultbound. pfa_gap_division_step_newmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_division_step_newmultiplyresultcongruence pfa_offset_right_division_step_newmultiplyresultcongruence. ((k) * (pfd_difference_division_step_new)) + (p) * pfa_offset_left_division_step_newmultiplyresultcongruence = (q) + (p) * pfa_offset_right_division_step_newmultiplyresultcongruence))))))))))))))))