prime_field_polynomial_quotient_step_functional

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc M qb qc i q r. (exists pfd_input_step_unique_first pfd_previous_step_unique_first pfd_difference_step_unique_first. ((((exists ff_h_pfp_step_unique_firstinput. ff_h_pfp_step_unique_firstinput + S (pfd_input_step_unique_first) = S ((S (i)) * ac)) /\ exists ff_q_pfp_step_unique_firstinput. ab = ff_q_pfp_step_unique_firstinput * S ((S (i)) * ac) + (pfd_input_step_unique_first))) /\ (((exists pfc_terms_code_step_unique_firstprevious pfc_terms_scale_step_unique_firstprevious pfc_natural_sum_step_unique_firstprevious. ((forall pfc_index_step_unique_firstpreviousdiagonal. (exists pfa_gap_step_unique_firstpreviousdiagonalbound. pfa_gap_step_unique_firstpreviousdiagonalbound + S (pfc_index_step_unique_firstpreviousdiagonal) = (S (i))) -> exists pfc_value_step_unique_firstpreviousdiagonal. ((((exists ff_h_pfp_step_unique_firstpreviousdiagonalentry. ff_h_pfp_step_unique_firstpreviousdiagonalentry + S (pfc_value_step_unique_firstpreviousdiagonal) = S ((S (pfc_index_step_unique_firstpreviousdiagonal)) * pfc_terms_scale_step_unique_firstprevious)) /\ exists ff_q_pfp_step_unique_firstpreviousdiagonalentry. pfc_terms_code_step_unique_firstprevious = ff_q_pfp_step_unique_firstpreviousdiagonalentry * S ((S (pfc_index_step_unique_firstpreviousdiagonal)) * pfc_terms_scale_step_unique_firstprevious) + (pfc_value_step_unique_firstpreviousdiagonal))) /\ ((exists pfc_complement_step_unique_firstpreviousdiagonalterm pfc_left_step_unique_firstpreviousdiagonalterm pfc_right_step_unique_firstpreviousdiagonalterm. (((pfc_index_step_unique_firstpreviousdiagonal)+pfc_complement_step_unique_firstpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_step_unique_firstpreviousdiagonaltermleftinside. pfa_gap_step_unique_firstpreviousdiagonaltermleftinside + S (pfc_index_step_unique_firstpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_step_unique_firstpreviousdiagonaltermleftentry. ff_h_pfp_step_unique_firstpreviousdiagonaltermleftentry + S (pfc_left_step_unique_firstpreviousdiagonalterm) = S ((S (pfc_index_step_unique_firstpreviousdiagonal)) * qc)) /\ exists ff_q_pfp_step_unique_firstpreviousdiagonaltermleftentry. qb = ff_q_pfp_step_unique_firstpreviousdiagonaltermleftentry * S ((S (pfc_index_step_unique_firstpreviousdiagonal)) * qc) + (pfc_left_step_unique_firstpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_firstpreviousdiagonaltermleftoutside. pfc_gap_step_unique_firstpreviousdiagonaltermleftoutside+(i)=(pfc_index_step_unique_firstpreviousdiagonal)) /\ (((pfc_left_step_unique_firstpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_step_unique_firstpreviousdiagonaltermrightinside. pfa_gap_step_unique_firstpreviousdiagonaltermrightinside + S (pfc_complement_step_unique_firstpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_step_unique_firstpreviousdiagonaltermrightentry. ff_h_pfp_step_unique_firstpreviousdiagonaltermrightentry + S (pfc_right_step_unique_firstpreviousdiagonalterm) = S ((S (pfc_complement_step_unique_firstpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_step_unique_firstpreviousdiagonaltermrightentry. bb = ff_q_pfp_step_unique_firstpreviousdiagonaltermrightentry * S ((S (pfc_complement_step_unique_firstpreviousdiagonalterm)) * bc) + (pfc_right_step_unique_firstpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_firstpreviousdiagonaltermrightoutside. pfc_gap_step_unique_firstpreviousdiagonaltermrightoutside+(M)=(pfc_complement_step_unique_firstpreviousdiagonalterm)) /\ (((pfc_right_step_unique_firstpreviousdiagonalterm)=0))))) /\ (((pfc_value_step_unique_firstpreviousdiagonal)=pfc_left_step_unique_firstpreviousdiagonalterm*pfc_right_step_unique_firstpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_step_unique_firstprevioussum fs_v_pfc_step_unique_firstprevioussum. ((((exists fs_h_pfc_step_unique_firstprevioussum_body_start. fs_h_pfc_step_unique_firstprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_step_unique_firstprevioussum)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_start. fs_u_pfc_step_unique_firstprevioussum = fs_q_pfc_step_unique_firstprevioussum_body_start * S ((S (0)) * fs_v_pfc_step_unique_firstprevioussum) + (0))) /\ ((((exists fs_h_pfc_step_unique_firstprevioussum_body_terminal. fs_h_pfc_step_unique_firstprevioussum_body_terminal + S (pfc_natural_sum_step_unique_firstprevious) = S ((S (S (i))) * fs_v_pfc_step_unique_firstprevioussum)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_terminal. fs_u_pfc_step_unique_firstprevioussum = fs_q_pfc_step_unique_firstprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_step_unique_firstprevioussum) + (pfc_natural_sum_step_unique_firstprevious))) /\ forall fs_i_pfc_step_unique_firstprevioussum_body_steps. (exists fs_lt_pfc_step_unique_firstprevioussum_body_steps_bound. fs_lt_pfc_step_unique_firstprevioussum_body_steps_bound + S fs_i_pfc_step_unique_firstprevioussum_body_steps = S (i)) -> exists fs_a_pfc_step_unique_firstprevioussum_body_steps fs_r_pfc_step_unique_firstprevioussum_body_steps fs_s_pfc_step_unique_firstprevioussum_body_steps. ((((exists fs_h_pfc_step_unique_firstprevioussum_body_steps_summand. fs_h_pfc_step_unique_firstprevioussum_body_steps_summand + S (fs_a_pfc_step_unique_firstprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_firstprevioussum_body_steps)) * pfc_terms_scale_step_unique_firstprevious)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_steps_summand. pfc_terms_code_step_unique_firstprevious = fs_q_pfc_step_unique_firstprevioussum_body_steps_summand * S ((S (fs_i_pfc_step_unique_firstprevioussum_body_steps)) * pfc_terms_scale_step_unique_firstprevious) + (fs_a_pfc_step_unique_firstprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_firstprevioussum_body_steps_partial. fs_h_pfc_step_unique_firstprevioussum_body_steps_partial + S (fs_r_pfc_step_unique_firstprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_firstprevioussum_body_steps)) * fs_v_pfc_step_unique_firstprevioussum)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_steps_partial. fs_u_pfc_step_unique_firstprevioussum = fs_q_pfc_step_unique_firstprevioussum_body_steps_partial * S ((S (fs_i_pfc_step_unique_firstprevioussum_body_steps)) * fs_v_pfc_step_unique_firstprevioussum) + (fs_r_pfc_step_unique_firstprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_firstprevioussum_body_steps_successor. fs_h_pfc_step_unique_firstprevioussum_body_steps_successor + S (fs_s_pfc_step_unique_firstprevioussum_body_steps) = S ((S (S fs_i_pfc_step_unique_firstprevioussum_body_steps)) * fs_v_pfc_step_unique_firstprevioussum)) /\ exists fs_q_pfc_step_unique_firstprevioussum_body_steps_successor. fs_u_pfc_step_unique_firstprevioussum = fs_q_pfc_step_unique_firstprevioussum_body_steps_successor * S ((S (S fs_i_pfc_step_unique_firstprevioussum_body_steps)) * fs_v_pfc_step_unique_firstprevioussum) + (fs_s_pfc_step_unique_firstprevioussum_body_steps))) /\ fs_s_pfc_step_unique_firstprevioussum_body_steps = fs_r_pfc_step_unique_firstprevioussum_body_steps + fs_a_pfc_step_unique_firstprevioussum_body_steps)))))) /\ ((((exists pfa_gap_step_unique_firstpreviousresiduebound. pfa_gap_step_unique_firstpreviousresiduebound + S (pfd_previous_step_unique_first) = (p)) /\ ((exists pfa_offset_left_step_unique_firstpreviousresiduecongruence pfa_offset_right_step_unique_firstpreviousresiduecongruence. (pfc_natural_sum_step_unique_firstprevious) + (p) * pfa_offset_left_step_unique_firstpreviousresiduecongruence = (pfd_previous_step_unique_first) + (p) * pfa_offset_right_step_unique_firstpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_step_unique_firstsubtractleft. pfa_gap_step_unique_firstsubtractleft + S (pfd_previous_step_unique_first) = (p)) /\ (((exists pfa_gap_step_unique_firstsubtractright. pfa_gap_step_unique_firstsubtractright + S (pfd_difference_step_unique_first) = (p)) /\ ((((exists pfa_gap_step_unique_firstsubtractresultbound. pfa_gap_step_unique_firstsubtractresultbound + S (pfd_input_step_unique_first) = (p)) /\ ((exists pfa_offset_left_step_unique_firstsubtractresultcongruence pfa_offset_right_step_unique_firstsubtractresultcongruence. ((pfd_previous_step_unique_first) + (pfd_difference_step_unique_first)) + (p) * pfa_offset_left_step_unique_firstsubtractresultcongruence = (pfd_input_step_unique_first) + (p) * pfa_offset_right_step_unique_firstsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_step_unique_firstmultiplyleft. pfa_gap_step_unique_firstmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_step_unique_firstmultiplyright. pfa_gap_step_unique_firstmultiplyright + S (pfd_difference_step_unique_first) = (p)) /\ ((((exists pfa_gap_step_unique_firstmultiplyresultbound. pfa_gap_step_unique_firstmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_step_unique_firstmultiplyresultcongruence pfa_offset_right_step_unique_firstmultiplyresultcongruence. ((k) * (pfd_difference_step_unique_first)) + (p) * pfa_offset_left_step_unique_firstmultiplyresultcongruence = (q) + (p) * pfa_offset_right_step_unique_firstmultiplyresultcongruence)))))))))))))))) -> (exists pfd_input_step_unique_second pfd_previous_step_unique_second pfd_difference_step_unique_second. ((((exists ff_h_pfp_step_unique_secondinput. ff_h_pfp_step_unique_secondinput + S (pfd_input_step_unique_second) = S ((S (i)) * ac)) /\ exists ff_q_pfp_step_unique_secondinput. ab = ff_q_pfp_step_unique_secondinput * S ((S (i)) * ac) + (pfd_input_step_unique_second))) /\ (((exists pfc_terms_code_step_unique_secondprevious pfc_terms_scale_step_unique_secondprevious pfc_natural_sum_step_unique_secondprevious. ((forall pfc_index_step_unique_secondpreviousdiagonal. (exists pfa_gap_step_unique_secondpreviousdiagonalbound. pfa_gap_step_unique_secondpreviousdiagonalbound + S (pfc_index_step_unique_secondpreviousdiagonal) = (S (i))) -> exists pfc_value_step_unique_secondpreviousdiagonal. ((((exists ff_h_pfp_step_unique_secondpreviousdiagonalentry. ff_h_pfp_step_unique_secondpreviousdiagonalentry + S (pfc_value_step_unique_secondpreviousdiagonal) = S ((S (pfc_index_step_unique_secondpreviousdiagonal)) * pfc_terms_scale_step_unique_secondprevious)) /\ exists ff_q_pfp_step_unique_secondpreviousdiagonalentry. pfc_terms_code_step_unique_secondprevious = ff_q_pfp_step_unique_secondpreviousdiagonalentry * S ((S (pfc_index_step_unique_secondpreviousdiagonal)) * pfc_terms_scale_step_unique_secondprevious) + (pfc_value_step_unique_secondpreviousdiagonal))) /\ ((exists pfc_complement_step_unique_secondpreviousdiagonalterm pfc_left_step_unique_secondpreviousdiagonalterm pfc_right_step_unique_secondpreviousdiagonalterm. (((pfc_index_step_unique_secondpreviousdiagonal)+pfc_complement_step_unique_secondpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_step_unique_secondpreviousdiagonaltermleftinside. pfa_gap_step_unique_secondpreviousdiagonaltermleftinside + S (pfc_index_step_unique_secondpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_step_unique_secondpreviousdiagonaltermleftentry. ff_h_pfp_step_unique_secondpreviousdiagonaltermleftentry + S (pfc_left_step_unique_secondpreviousdiagonalterm) = S ((S (pfc_index_step_unique_secondpreviousdiagonal)) * qc)) /\ exists ff_q_pfp_step_unique_secondpreviousdiagonaltermleftentry. qb = ff_q_pfp_step_unique_secondpreviousdiagonaltermleftentry * S ((S (pfc_index_step_unique_secondpreviousdiagonal)) * qc) + (pfc_left_step_unique_secondpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_secondpreviousdiagonaltermleftoutside. pfc_gap_step_unique_secondpreviousdiagonaltermleftoutside+(i)=(pfc_index_step_unique_secondpreviousdiagonal)) /\ (((pfc_left_step_unique_secondpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_step_unique_secondpreviousdiagonaltermrightinside. pfa_gap_step_unique_secondpreviousdiagonaltermrightinside + S (pfc_complement_step_unique_secondpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_step_unique_secondpreviousdiagonaltermrightentry. ff_h_pfp_step_unique_secondpreviousdiagonaltermrightentry + S (pfc_right_step_unique_secondpreviousdiagonalterm) = S ((S (pfc_complement_step_unique_secondpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_step_unique_secondpreviousdiagonaltermrightentry. bb = ff_q_pfp_step_unique_secondpreviousdiagonaltermrightentry * S ((S (pfc_complement_step_unique_secondpreviousdiagonalterm)) * bc) + (pfc_right_step_unique_secondpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_secondpreviousdiagonaltermrightoutside. pfc_gap_step_unique_secondpreviousdiagonaltermrightoutside+(M)=(pfc_complement_step_unique_secondpreviousdiagonalterm)) /\ (((pfc_right_step_unique_secondpreviousdiagonalterm)=0))))) /\ (((pfc_value_step_unique_secondpreviousdiagonal)=pfc_left_step_unique_secondpreviousdiagonalterm*pfc_right_step_unique_secondpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_step_unique_secondprevioussum fs_v_pfc_step_unique_secondprevioussum. ((((exists fs_h_pfc_step_unique_secondprevioussum_body_start. fs_h_pfc_step_unique_secondprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_step_unique_secondprevioussum)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_start. fs_u_pfc_step_unique_secondprevioussum = fs_q_pfc_step_unique_secondprevioussum_body_start * S ((S (0)) * fs_v_pfc_step_unique_secondprevioussum) + (0))) /\ ((((exists fs_h_pfc_step_unique_secondprevioussum_body_terminal. fs_h_pfc_step_unique_secondprevioussum_body_terminal + S (pfc_natural_sum_step_unique_secondprevious) = S ((S (S (i))) * fs_v_pfc_step_unique_secondprevioussum)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_terminal. fs_u_pfc_step_unique_secondprevioussum = fs_q_pfc_step_unique_secondprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_step_unique_secondprevioussum) + (pfc_natural_sum_step_unique_secondprevious))) /\ forall fs_i_pfc_step_unique_secondprevioussum_body_steps. (exists fs_lt_pfc_step_unique_secondprevioussum_body_steps_bound. fs_lt_pfc_step_unique_secondprevioussum_body_steps_bound + S fs_i_pfc_step_unique_secondprevioussum_body_steps = S (i)) -> exists fs_a_pfc_step_unique_secondprevioussum_body_steps fs_r_pfc_step_unique_secondprevioussum_body_steps fs_s_pfc_step_unique_secondprevioussum_body_steps. ((((exists fs_h_pfc_step_unique_secondprevioussum_body_steps_summand. fs_h_pfc_step_unique_secondprevioussum_body_steps_summand + S (fs_a_pfc_step_unique_secondprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_secondprevioussum_body_steps)) * pfc_terms_scale_step_unique_secondprevious)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_steps_summand. pfc_terms_code_step_unique_secondprevious = fs_q_pfc_step_unique_secondprevioussum_body_steps_summand * S ((S (fs_i_pfc_step_unique_secondprevioussum_body_steps)) * pfc_terms_scale_step_unique_secondprevious) + (fs_a_pfc_step_unique_secondprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_secondprevioussum_body_steps_partial. fs_h_pfc_step_unique_secondprevioussum_body_steps_partial + S (fs_r_pfc_step_unique_secondprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_secondprevioussum_body_steps)) * fs_v_pfc_step_unique_secondprevioussum)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_steps_partial. fs_u_pfc_step_unique_secondprevioussum = fs_q_pfc_step_unique_secondprevioussum_body_steps_partial * S ((S (fs_i_pfc_step_unique_secondprevioussum_body_steps)) * fs_v_pfc_step_unique_secondprevioussum) + (fs_r_pfc_step_unique_secondprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_secondprevioussum_body_steps_successor. fs_h_pfc_step_unique_secondprevioussum_body_steps_successor + S (fs_s_pfc_step_unique_secondprevioussum_body_steps) = S ((S (S fs_i_pfc_step_unique_secondprevioussum_body_steps)) * fs_v_pfc_step_unique_secondprevioussum)) /\ exists fs_q_pfc_step_unique_secondprevioussum_body_steps_successor. fs_u_pfc_step_unique_secondprevioussum = fs_q_pfc_step_unique_secondprevioussum_body_steps_successor * S ((S (S fs_i_pfc_step_unique_secondprevioussum_body_steps)) * fs_v_pfc_step_unique_secondprevioussum) + (fs_s_pfc_step_unique_secondprevioussum_body_steps))) /\ fs_s_pfc_step_unique_secondprevioussum_body_steps = fs_r_pfc_step_unique_secondprevioussum_body_steps + fs_a_pfc_step_unique_secondprevioussum_body_steps)))))) /\ ((((exists pfa_gap_step_unique_secondpreviousresiduebound. pfa_gap_step_unique_secondpreviousresiduebound + S (pfd_previous_step_unique_second) = (p)) /\ ((exists pfa_offset_left_step_unique_secondpreviousresiduecongruence pfa_offset_right_step_unique_secondpreviousresiduecongruence. (pfc_natural_sum_step_unique_secondprevious) + (p) * pfa_offset_left_step_unique_secondpreviousresiduecongruence = (pfd_previous_step_unique_second) + (p) * pfa_offset_right_step_unique_secondpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_step_unique_secondsubtractleft. pfa_gap_step_unique_secondsubtractleft + S (pfd_previous_step_unique_second) = (p)) /\ (((exists pfa_gap_step_unique_secondsubtractright. pfa_gap_step_unique_secondsubtractright + S (pfd_difference_step_unique_second) = (p)) /\ ((((exists pfa_gap_step_unique_secondsubtractresultbound. pfa_gap_step_unique_secondsubtractresultbound + S (pfd_input_step_unique_second) = (p)) /\ ((exists pfa_offset_left_step_unique_secondsubtractresultcongruence pfa_offset_right_step_unique_secondsubtractresultcongruence. ((pfd_previous_step_unique_second) + (pfd_difference_step_unique_second)) + (p) * pfa_offset_left_step_unique_secondsubtractresultcongruence = (pfd_input_step_unique_second) + (p) * pfa_offset_right_step_unique_secondsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_step_unique_secondmultiplyleft. pfa_gap_step_unique_secondmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_step_unique_secondmultiplyright. pfa_gap_step_unique_secondmultiplyright + S (pfd_difference_step_unique_second) = (p)) /\ ((((exists pfa_gap_step_unique_secondmultiplyresultbound. pfa_gap_step_unique_secondmultiplyresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_step_unique_secondmultiplyresultcongruence pfa_offset_right_step_unique_secondmultiplyresultcongruence. ((k) * (pfd_difference_step_unique_second)) + (p) * pfa_offset_left_step_unique_secondmultiplyresultcongruence = (r) + (p) * pfa_offset_right_step_unique_secondmultiplyresultcongruence)))))))))))))))) -> q=r