prime_field_polynomial_quotient_prefix_empty

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc M qb qc. forall pfd_index_division_empty. (exists pfa_gap_division_emptybound. pfa_gap_division_emptybound + S (pfd_index_division_empty) = (0)) -> exists pfd_value_division_empty. ((((exists ff_h_pfp_division_emptyentry. ff_h_pfp_division_emptyentry + S (pfd_value_division_empty) = S ((S (pfd_index_division_empty)) * qc)) /\ exists ff_q_pfp_division_emptyentry. qb = ff_q_pfp_division_emptyentry * S ((S (pfd_index_division_empty)) * qc) + (pfd_value_division_empty))) /\ ((exists pfd_input_division_emptystep pfd_previous_division_emptystep pfd_difference_division_emptystep. ((((exists ff_h_pfp_division_emptystepinput. ff_h_pfp_division_emptystepinput + S (pfd_input_division_emptystep) = S ((S (pfd_index_division_empty)) * ac)) /\ exists ff_q_pfp_division_emptystepinput. ab = ff_q_pfp_division_emptystepinput * S ((S (pfd_index_division_empty)) * ac) + (pfd_input_division_emptystep))) /\ (((exists pfc_terms_code_division_emptystepprevious pfc_terms_scale_division_emptystepprevious pfc_natural_sum_division_emptystepprevious. ((forall pfc_index_division_emptysteppreviousdiagonal. (exists pfa_gap_division_emptysteppreviousdiagonalbound. pfa_gap_division_emptysteppreviousdiagonalbound + S (pfc_index_division_emptysteppreviousdiagonal) = (S (pfd_index_division_empty))) -> exists pfc_value_division_emptysteppreviousdiagonal. ((((exists ff_h_pfp_division_emptysteppreviousdiagonalentry. ff_h_pfp_division_emptysteppreviousdiagonalentry + S (pfc_value_division_emptysteppreviousdiagonal) = S ((S (pfc_index_division_emptysteppreviousdiagonal)) * pfc_terms_scale_division_emptystepprevious)) /\ exists ff_q_pfp_division_emptysteppreviousdiagonalentry. pfc_terms_code_division_emptystepprevious = ff_q_pfp_division_emptysteppreviousdiagonalentry * S ((S (pfc_index_division_emptysteppreviousdiagonal)) * pfc_terms_scale_division_emptystepprevious) + (pfc_value_division_emptysteppreviousdiagonal))) /\ ((exists pfc_complement_division_emptysteppreviousdiagonalterm pfc_left_division_emptysteppreviousdiagonalterm pfc_right_division_emptysteppreviousdiagonalterm. (((pfc_index_division_emptysteppreviousdiagonal)+pfc_complement_division_emptysteppreviousdiagonalterm=(pfd_index_division_empty)) /\ ((((((exists pfa_gap_division_emptysteppreviousdiagonaltermleftinside. pfa_gap_division_emptysteppreviousdiagonaltermleftinside + S (pfc_index_division_emptysteppreviousdiagonal) = (pfd_index_division_empty)) /\ ((((exists ff_h_pfp_division_emptysteppreviousdiagonaltermleftentry. ff_h_pfp_division_emptysteppreviousdiagonaltermleftentry + S (pfc_left_division_emptysteppreviousdiagonalterm) = S ((S (pfc_index_division_emptysteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_emptysteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_emptysteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_emptysteppreviousdiagonal)) * qc) + (pfc_left_division_emptysteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_emptysteppreviousdiagonaltermleftoutside. pfc_gap_division_emptysteppreviousdiagonaltermleftoutside+(pfd_index_division_empty)=(pfc_index_division_emptysteppreviousdiagonal)) /\ (((pfc_left_division_emptysteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_emptysteppreviousdiagonaltermrightinside. pfa_gap_division_emptysteppreviousdiagonaltermrightinside + S (pfc_complement_division_emptysteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_emptysteppreviousdiagonaltermrightentry. ff_h_pfp_division_emptysteppreviousdiagonaltermrightentry + S (pfc_right_division_emptysteppreviousdiagonalterm) = S ((S (pfc_complement_division_emptysteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_emptysteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_emptysteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_emptysteppreviousdiagonalterm)) * bc) + (pfc_right_division_emptysteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_emptysteppreviousdiagonaltermrightoutside. pfc_gap_division_emptysteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_emptysteppreviousdiagonalterm)) /\ (((pfc_right_division_emptysteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_emptysteppreviousdiagonal)=pfc_left_division_emptysteppreviousdiagonalterm*pfc_right_division_emptysteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_emptystepprevioussum fs_v_pfc_division_emptystepprevioussum. ((((exists fs_h_pfc_division_emptystepprevioussum_body_start. fs_h_pfc_division_emptystepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_emptystepprevioussum)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_start. fs_u_pfc_division_emptystepprevioussum = fs_q_pfc_division_emptystepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_emptystepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_emptystepprevioussum_body_terminal. fs_h_pfc_division_emptystepprevioussum_body_terminal + S (pfc_natural_sum_division_emptystepprevious) = S ((S (S (pfd_index_division_empty))) * fs_v_pfc_division_emptystepprevioussum)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_terminal. fs_u_pfc_division_emptystepprevioussum = fs_q_pfc_division_emptystepprevioussum_body_terminal * S ((S (S (pfd_index_division_empty))) * fs_v_pfc_division_emptystepprevioussum) + (pfc_natural_sum_division_emptystepprevious))) /\ forall fs_i_pfc_division_emptystepprevioussum_body_steps. (exists fs_lt_pfc_division_emptystepprevioussum_body_steps_bound. fs_lt_pfc_division_emptystepprevioussum_body_steps_bound + S fs_i_pfc_division_emptystepprevioussum_body_steps = S (pfd_index_division_empty)) -> exists fs_a_pfc_division_emptystepprevioussum_body_steps fs_r_pfc_division_emptystepprevioussum_body_steps fs_s_pfc_division_emptystepprevioussum_body_steps. ((((exists fs_h_pfc_division_emptystepprevioussum_body_steps_summand. fs_h_pfc_division_emptystepprevioussum_body_steps_summand + S (fs_a_pfc_division_emptystepprevioussum_body_steps) = S ((S (fs_i_pfc_division_emptystepprevioussum_body_steps)) * pfc_terms_scale_division_emptystepprevious)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_steps_summand. pfc_terms_code_division_emptystepprevious = fs_q_pfc_division_emptystepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_emptystepprevioussum_body_steps)) * pfc_terms_scale_division_emptystepprevious) + (fs_a_pfc_division_emptystepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_emptystepprevioussum_body_steps_partial. fs_h_pfc_division_emptystepprevioussum_body_steps_partial + S (fs_r_pfc_division_emptystepprevioussum_body_steps) = S ((S (fs_i_pfc_division_emptystepprevioussum_body_steps)) * fs_v_pfc_division_emptystepprevioussum)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_steps_partial. fs_u_pfc_division_emptystepprevioussum = fs_q_pfc_division_emptystepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_emptystepprevioussum_body_steps)) * fs_v_pfc_division_emptystepprevioussum) + (fs_r_pfc_division_emptystepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_emptystepprevioussum_body_steps_successor. fs_h_pfc_division_emptystepprevioussum_body_steps_successor + S (fs_s_pfc_division_emptystepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_emptystepprevioussum_body_steps)) * fs_v_pfc_division_emptystepprevioussum)) /\ exists fs_q_pfc_division_emptystepprevioussum_body_steps_successor. fs_u_pfc_division_emptystepprevioussum = fs_q_pfc_division_emptystepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_emptystepprevioussum_body_steps)) * fs_v_pfc_division_emptystepprevioussum) + (fs_s_pfc_division_emptystepprevioussum_body_steps))) /\ fs_s_pfc_division_emptystepprevioussum_body_steps = fs_r_pfc_division_emptystepprevioussum_body_steps + fs_a_pfc_division_emptystepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_emptysteppreviousresiduebound. pfa_gap_division_emptysteppreviousresiduebound + S (pfd_previous_division_emptystep) = (p)) /\ ((exists pfa_offset_left_division_emptysteppreviousresiduecongruence pfa_offset_right_division_emptysteppreviousresiduecongruence. (pfc_natural_sum_division_emptystepprevious) + (p) * pfa_offset_left_division_emptysteppreviousresiduecongruence = (pfd_previous_division_emptystep) + (p) * pfa_offset_right_division_emptysteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_emptystepsubtractleft. pfa_gap_division_emptystepsubtractleft + S (pfd_previous_division_emptystep) = (p)) /\ (((exists pfa_gap_division_emptystepsubtractright. pfa_gap_division_emptystepsubtractright + S (pfd_difference_division_emptystep) = (p)) /\ ((((exists pfa_gap_division_emptystepsubtractresultbound. pfa_gap_division_emptystepsubtractresultbound + S (pfd_input_division_emptystep) = (p)) /\ ((exists pfa_offset_left_division_emptystepsubtractresultcongruence pfa_offset_right_division_emptystepsubtractresultcongruence. ((pfd_previous_division_emptystep) + (pfd_difference_division_emptystep)) + (p) * pfa_offset_left_division_emptystepsubtractresultcongruence = (pfd_input_division_emptystep) + (p) * pfa_offset_right_division_emptystepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_emptystepmultiplyleft. pfa_gap_division_emptystepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_emptystepmultiplyright. pfa_gap_division_emptystepmultiplyright + S (pfd_difference_division_emptystep) = (p)) /\ ((((exists pfa_gap_division_emptystepmultiplyresultbound. pfa_gap_division_emptystepmultiplyresultbound + S (pfd_value_division_empty) = (p)) /\ ((exists pfa_offset_left_division_emptystepmultiplyresultcongruence pfa_offset_right_division_emptystepmultiplyresultcongruence. ((k) * (pfd_difference_division_emptystep)) + (p) * pfa_offset_left_division_emptystepmultiplyresultcongruence = (pfd_value_division_empty) + (p) * pfa_offset_right_division_emptystepmultiplyresultcongruence))))))))))))))))))