prime_field_polynomial_quotient_prefix_restrict

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc M qb qc N K. (exists pfc_gap_division_restrict_bound. pfc_gap_division_restrict_bound+(K)=(N)) -> (forall pfd_index_division_restrict_old. (exists pfa_gap_division_restrict_oldbound. pfa_gap_division_restrict_oldbound + S (pfd_index_division_restrict_old) = (N)) -> exists pfd_value_division_restrict_old. ((((exists ff_h_pfp_division_restrict_oldentry. ff_h_pfp_division_restrict_oldentry + S (pfd_value_division_restrict_old) = S ((S (pfd_index_division_restrict_old)) * qc)) /\ exists ff_q_pfp_division_restrict_oldentry. qb = ff_q_pfp_division_restrict_oldentry * S ((S (pfd_index_division_restrict_old)) * qc) + (pfd_value_division_restrict_old))) /\ ((exists pfd_input_division_restrict_oldstep pfd_previous_division_restrict_oldstep pfd_difference_division_restrict_oldstep. ((((exists ff_h_pfp_division_restrict_oldstepinput. ff_h_pfp_division_restrict_oldstepinput + S (pfd_input_division_restrict_oldstep) = S ((S (pfd_index_division_restrict_old)) * ac)) /\ exists ff_q_pfp_division_restrict_oldstepinput. ab = ff_q_pfp_division_restrict_oldstepinput * S ((S (pfd_index_division_restrict_old)) * ac) + (pfd_input_division_restrict_oldstep))) /\ (((exists pfc_terms_code_division_restrict_oldstepprevious pfc_terms_scale_division_restrict_oldstepprevious pfc_natural_sum_division_restrict_oldstepprevious. ((forall pfc_index_division_restrict_oldsteppreviousdiagonal. (exists pfa_gap_division_restrict_oldsteppreviousdiagonalbound. pfa_gap_division_restrict_oldsteppreviousdiagonalbound + S (pfc_index_division_restrict_oldsteppreviousdiagonal) = (S (pfd_index_division_restrict_old))) -> exists pfc_value_division_restrict_oldsteppreviousdiagonal. ((((exists ff_h_pfp_division_restrict_oldsteppreviousdiagonalentry. ff_h_pfp_division_restrict_oldsteppreviousdiagonalentry + S (pfc_value_division_restrict_oldsteppreviousdiagonal) = S ((S (pfc_index_division_restrict_oldsteppreviousdiagonal)) * pfc_terms_scale_division_restrict_oldstepprevious)) /\ exists ff_q_pfp_division_restrict_oldsteppreviousdiagonalentry. pfc_terms_code_division_restrict_oldstepprevious = ff_q_pfp_division_restrict_oldsteppreviousdiagonalentry * S ((S (pfc_index_division_restrict_oldsteppreviousdiagonal)) * pfc_terms_scale_division_restrict_oldstepprevious) + (pfc_value_division_restrict_oldsteppreviousdiagonal))) /\ ((exists pfc_complement_division_restrict_oldsteppreviousdiagonalterm pfc_left_division_restrict_oldsteppreviousdiagonalterm pfc_right_division_restrict_oldsteppreviousdiagonalterm. (((pfc_index_division_restrict_oldsteppreviousdiagonal)+pfc_complement_division_restrict_oldsteppreviousdiagonalterm=(pfd_index_division_restrict_old)) /\ ((((((exists pfa_gap_division_restrict_oldsteppreviousdiagonaltermleftinside. pfa_gap_division_restrict_oldsteppreviousdiagonaltermleftinside + S (pfc_index_division_restrict_oldsteppreviousdiagonal) = (pfd_index_division_restrict_old)) /\ ((((exists ff_h_pfp_division_restrict_oldsteppreviousdiagonaltermleftentry. ff_h_pfp_division_restrict_oldsteppreviousdiagonaltermleftentry + S (pfc_left_division_restrict_oldsteppreviousdiagonalterm) = S ((S (pfc_index_division_restrict_oldsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_restrict_oldsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_restrict_oldsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_restrict_oldsteppreviousdiagonal)) * qc) + (pfc_left_division_restrict_oldsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_restrict_oldsteppreviousdiagonaltermleftoutside. pfc_gap_division_restrict_oldsteppreviousdiagonaltermleftoutside+(pfd_index_division_restrict_old)=(pfc_index_division_restrict_oldsteppreviousdiagonal)) /\ (((pfc_left_division_restrict_oldsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_restrict_oldsteppreviousdiagonaltermrightinside. pfa_gap_division_restrict_oldsteppreviousdiagonaltermrightinside + S (pfc_complement_division_restrict_oldsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_restrict_oldsteppreviousdiagonaltermrightentry. ff_h_pfp_division_restrict_oldsteppreviousdiagonaltermrightentry + S (pfc_right_division_restrict_oldsteppreviousdiagonalterm) = S ((S (pfc_complement_division_restrict_oldsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_restrict_oldsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_restrict_oldsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_restrict_oldsteppreviousdiagonalterm)) * bc) + (pfc_right_division_restrict_oldsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_restrict_oldsteppreviousdiagonaltermrightoutside. pfc_gap_division_restrict_oldsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_restrict_oldsteppreviousdiagonalterm)) /\ (((pfc_right_division_restrict_oldsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_restrict_oldsteppreviousdiagonal)=pfc_left_division_restrict_oldsteppreviousdiagonalterm*pfc_right_division_restrict_oldsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_restrict_oldstepprevioussum fs_v_pfc_division_restrict_oldstepprevioussum. ((((exists fs_h_pfc_division_restrict_oldstepprevioussum_body_start. fs_h_pfc_division_restrict_oldstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_restrict_oldstepprevioussum)) /\ exists fs_q_pfc_division_restrict_oldstepprevioussum_body_start. fs_u_pfc_division_restrict_oldstepprevioussum = fs_q_pfc_division_restrict_oldstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_restrict_oldstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_restrict_oldstepprevioussum_body_terminal. fs_h_pfc_division_restrict_oldstepprevioussum_body_terminal + S (pfc_natural_sum_division_restrict_oldstepprevious) = S ((S (S (pfd_index_division_restrict_old))) * fs_v_pfc_division_restrict_oldstepprevioussum)) /\ exists fs_q_pfc_division_restrict_oldstepprevioussum_body_terminal. fs_u_pfc_division_restrict_oldstepprevioussum = fs_q_pfc_division_restrict_oldstepprevioussum_body_terminal * S ((S (S (pfd_index_division_restrict_old))) * fs_v_pfc_division_restrict_oldstepprevioussum) + (pfc_natural_sum_division_restrict_oldstepprevious))) /\ forall fs_i_pfc_division_restrict_oldstepprevioussum_body_steps. (exists fs_lt_pfc_division_restrict_oldstepprevioussum_body_steps_bound. fs_lt_pfc_division_restrict_oldstepprevioussum_body_steps_bound + S fs_i_pfc_division_restrict_oldstepprevioussum_body_steps = S (pfd_index_division_restrict_old)) -> exists fs_a_pfc_division_restrict_oldstepprevioussum_body_steps fs_r_pfc_division_restrict_oldstepprevioussum_body_steps fs_s_pfc_division_restrict_oldstepprevioussum_body_steps. ((((exists fs_h_pfc_division_restrict_oldstepprevioussum_body_steps_summand. fs_h_pfc_division_restrict_oldstepprevioussum_body_steps_summand + S (fs_a_pfc_division_restrict_oldstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_restrict_oldstepprevioussum_body_steps)) * pfc_terms_scale_division_restrict_oldstepprevious)) /\ exists fs_q_pfc_division_restrict_oldstepprevioussum_body_steps_summand. pfc_terms_code_division_restrict_oldstepprevious = fs_q_pfc_division_restrict_oldstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_restrict_oldstepprevioussum_body_steps)) * pfc_terms_scale_division_restrict_oldstepprevious) + (fs_a_pfc_division_restrict_oldstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_restrict_oldstepprevioussum_body_steps_partial. fs_h_pfc_division_restrict_oldstepprevioussum_body_steps_partial + S (fs_r_pfc_division_restrict_oldstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_restrict_oldstepprevioussum_body_steps)) * fs_v_pfc_division_restrict_oldstepprevioussum)) /\ exists fs_q_pfc_division_restrict_oldstepprevioussum_body_steps_partial. fs_u_pfc_division_restrict_oldstepprevioussum = fs_q_pfc_division_restrict_oldstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_restrict_oldstepprevioussum_body_steps)) * fs_v_pfc_division_restrict_oldstepprevioussum) + (fs_r_pfc_division_restrict_oldstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_restrict_oldstepprevioussum_body_steps_successor. fs_h_pfc_division_restrict_oldstepprevioussum_body_steps_successor + S (fs_s_pfc_division_restrict_oldstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_restrict_oldstepprevioussum_body_steps)) * fs_v_pfc_division_restrict_oldstepprevioussum)) /\ exists fs_q_pfc_division_restrict_oldstepprevioussum_body_steps_successor. fs_u_pfc_division_restrict_oldstepprevioussum = fs_q_pfc_division_restrict_oldstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_restrict_oldstepprevioussum_body_steps)) * fs_v_pfc_division_restrict_oldstepprevioussum) + (fs_s_pfc_division_restrict_oldstepprevioussum_body_steps))) /\ fs_s_pfc_division_restrict_oldstepprevioussum_body_steps = fs_r_pfc_division_restrict_oldstepprevioussum_body_steps + fs_a_pfc_division_restrict_oldstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_restrict_oldsteppreviousresiduebound. pfa_gap_division_restrict_oldsteppreviousresiduebound + S (pfd_previous_division_restrict_oldstep) = (p)) /\ ((exists pfa_offset_left_division_restrict_oldsteppreviousresiduecongruence pfa_offset_right_division_restrict_oldsteppreviousresiduecongruence. (pfc_natural_sum_division_restrict_oldstepprevious) + (p) * pfa_offset_left_division_restrict_oldsteppreviousresiduecongruence = (pfd_previous_division_restrict_oldstep) + (p) * pfa_offset_right_division_restrict_oldsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_restrict_oldstepsubtractleft. pfa_gap_division_restrict_oldstepsubtractleft + S (pfd_previous_division_restrict_oldstep) = (p)) /\ (((exists pfa_gap_division_restrict_oldstepsubtractright. pfa_gap_division_restrict_oldstepsubtractright + S (pfd_difference_division_restrict_oldstep) = (p)) /\ ((((exists pfa_gap_division_restrict_oldstepsubtractresultbound. pfa_gap_division_restrict_oldstepsubtractresultbound + S (pfd_input_division_restrict_oldstep) = (p)) /\ ((exists pfa_offset_left_division_restrict_oldstepsubtractresultcongruence pfa_offset_right_division_restrict_oldstepsubtractresultcongruence. ((pfd_previous_division_restrict_oldstep) + (pfd_difference_division_restrict_oldstep)) + (p) * pfa_offset_left_division_restrict_oldstepsubtractresultcongruence = (pfd_input_division_restrict_oldstep) + (p) * pfa_offset_right_division_restrict_oldstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_restrict_oldstepmultiplyleft. pfa_gap_division_restrict_oldstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_restrict_oldstepmultiplyright. pfa_gap_division_restrict_oldstepmultiplyright + S (pfd_difference_division_restrict_oldstep) = (p)) /\ ((((exists pfa_gap_division_restrict_oldstepmultiplyresultbound. pfa_gap_division_restrict_oldstepmultiplyresultbound + S (pfd_value_division_restrict_old) = (p)) /\ ((exists pfa_offset_left_division_restrict_oldstepmultiplyresultcongruence pfa_offset_right_division_restrict_oldstepmultiplyresultcongruence. ((k) * (pfd_difference_division_restrict_oldstep)) + (p) * pfa_offset_left_division_restrict_oldstepmultiplyresultcongruence = (pfd_value_division_restrict_old) + (p) * pfa_offset_right_division_restrict_oldstepmultiplyresultcongruence))))))))))))))))))) -> (forall pfd_index_division_restrict_new. (exists pfa_gap_division_restrict_newbound. pfa_gap_division_restrict_newbound + S (pfd_index_division_restrict_new) = (K)) -> exists pfd_value_division_restrict_new. ((((exists ff_h_pfp_division_restrict_newentry. ff_h_pfp_division_restrict_newentry + S (pfd_value_division_restrict_new) = S ((S (pfd_index_division_restrict_new)) * qc)) /\ exists ff_q_pfp_division_restrict_newentry. qb = ff_q_pfp_division_restrict_newentry * S ((S (pfd_index_division_restrict_new)) * qc) + (pfd_value_division_restrict_new))) /\ ((exists pfd_input_division_restrict_newstep pfd_previous_division_restrict_newstep pfd_difference_division_restrict_newstep. ((((exists ff_h_pfp_division_restrict_newstepinput. ff_h_pfp_division_restrict_newstepinput + S (pfd_input_division_restrict_newstep) = S ((S (pfd_index_division_restrict_new)) * ac)) /\ exists ff_q_pfp_division_restrict_newstepinput. ab = ff_q_pfp_division_restrict_newstepinput * S ((S (pfd_index_division_restrict_new)) * ac) + (pfd_input_division_restrict_newstep))) /\ (((exists pfc_terms_code_division_restrict_newstepprevious pfc_terms_scale_division_restrict_newstepprevious pfc_natural_sum_division_restrict_newstepprevious. ((forall pfc_index_division_restrict_newsteppreviousdiagonal. (exists pfa_gap_division_restrict_newsteppreviousdiagonalbound. pfa_gap_division_restrict_newsteppreviousdiagonalbound + S (pfc_index_division_restrict_newsteppreviousdiagonal) = (S (pfd_index_division_restrict_new))) -> exists pfc_value_division_restrict_newsteppreviousdiagonal. ((((exists ff_h_pfp_division_restrict_newsteppreviousdiagonalentry. ff_h_pfp_division_restrict_newsteppreviousdiagonalentry + S (pfc_value_division_restrict_newsteppreviousdiagonal) = S ((S (pfc_index_division_restrict_newsteppreviousdiagonal)) * pfc_terms_scale_division_restrict_newstepprevious)) /\ exists ff_q_pfp_division_restrict_newsteppreviousdiagonalentry. pfc_terms_code_division_restrict_newstepprevious = ff_q_pfp_division_restrict_newsteppreviousdiagonalentry * S ((S (pfc_index_division_restrict_newsteppreviousdiagonal)) * pfc_terms_scale_division_restrict_newstepprevious) + (pfc_value_division_restrict_newsteppreviousdiagonal))) /\ ((exists pfc_complement_division_restrict_newsteppreviousdiagonalterm pfc_left_division_restrict_newsteppreviousdiagonalterm pfc_right_division_restrict_newsteppreviousdiagonalterm. (((pfc_index_division_restrict_newsteppreviousdiagonal)+pfc_complement_division_restrict_newsteppreviousdiagonalterm=(pfd_index_division_restrict_new)) /\ ((((((exists pfa_gap_division_restrict_newsteppreviousdiagonaltermleftinside. pfa_gap_division_restrict_newsteppreviousdiagonaltermleftinside + S (pfc_index_division_restrict_newsteppreviousdiagonal) = (pfd_index_division_restrict_new)) /\ ((((exists ff_h_pfp_division_restrict_newsteppreviousdiagonaltermleftentry. ff_h_pfp_division_restrict_newsteppreviousdiagonaltermleftentry + S (pfc_left_division_restrict_newsteppreviousdiagonalterm) = S ((S (pfc_index_division_restrict_newsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_restrict_newsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_restrict_newsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_restrict_newsteppreviousdiagonal)) * qc) + (pfc_left_division_restrict_newsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_restrict_newsteppreviousdiagonaltermleftoutside. pfc_gap_division_restrict_newsteppreviousdiagonaltermleftoutside+(pfd_index_division_restrict_new)=(pfc_index_division_restrict_newsteppreviousdiagonal)) /\ (((pfc_left_division_restrict_newsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_restrict_newsteppreviousdiagonaltermrightinside. pfa_gap_division_restrict_newsteppreviousdiagonaltermrightinside + S (pfc_complement_division_restrict_newsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_restrict_newsteppreviousdiagonaltermrightentry. ff_h_pfp_division_restrict_newsteppreviousdiagonaltermrightentry + S (pfc_right_division_restrict_newsteppreviousdiagonalterm) = S ((S (pfc_complement_division_restrict_newsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_restrict_newsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_restrict_newsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_restrict_newsteppreviousdiagonalterm)) * bc) + (pfc_right_division_restrict_newsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_restrict_newsteppreviousdiagonaltermrightoutside. pfc_gap_division_restrict_newsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_restrict_newsteppreviousdiagonalterm)) /\ (((pfc_right_division_restrict_newsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_restrict_newsteppreviousdiagonal)=pfc_left_division_restrict_newsteppreviousdiagonalterm*pfc_right_division_restrict_newsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_restrict_newstepprevioussum fs_v_pfc_division_restrict_newstepprevioussum. ((((exists fs_h_pfc_division_restrict_newstepprevioussum_body_start. fs_h_pfc_division_restrict_newstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_restrict_newstepprevioussum)) /\ exists fs_q_pfc_division_restrict_newstepprevioussum_body_start. fs_u_pfc_division_restrict_newstepprevioussum = fs_q_pfc_division_restrict_newstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_restrict_newstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_restrict_newstepprevioussum_body_terminal. fs_h_pfc_division_restrict_newstepprevioussum_body_terminal + S (pfc_natural_sum_division_restrict_newstepprevious) = S ((S (S (pfd_index_division_restrict_new))) * fs_v_pfc_division_restrict_newstepprevioussum)) /\ exists fs_q_pfc_division_restrict_newstepprevioussum_body_terminal. fs_u_pfc_division_restrict_newstepprevioussum = fs_q_pfc_division_restrict_newstepprevioussum_body_terminal * S ((S (S (pfd_index_division_restrict_new))) * fs_v_pfc_division_restrict_newstepprevioussum) + (pfc_natural_sum_division_restrict_newstepprevious))) /\ forall fs_i_pfc_division_restrict_newstepprevioussum_body_steps. (exists fs_lt_pfc_division_restrict_newstepprevioussum_body_steps_bound. fs_lt_pfc_division_restrict_newstepprevioussum_body_steps_bound + S fs_i_pfc_division_restrict_newstepprevioussum_body_steps = S (pfd_index_division_restrict_new)) -> exists fs_a_pfc_division_restrict_newstepprevioussum_body_steps fs_r_pfc_division_restrict_newstepprevioussum_body_steps fs_s_pfc_division_restrict_newstepprevioussum_body_steps. ((((exists fs_h_pfc_division_restrict_newstepprevioussum_body_steps_summand. fs_h_pfc_division_restrict_newstepprevioussum_body_steps_summand + S (fs_a_pfc_division_restrict_newstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_restrict_newstepprevioussum_body_steps)) * pfc_terms_scale_division_restrict_newstepprevious)) /\ exists fs_q_pfc_division_restrict_newstepprevioussum_body_steps_summand. pfc_terms_code_division_restrict_newstepprevious = fs_q_pfc_division_restrict_newstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_restrict_newstepprevioussum_body_steps)) * pfc_terms_scale_division_restrict_newstepprevious) + (fs_a_pfc_division_restrict_newstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_restrict_newstepprevioussum_body_steps_partial. fs_h_pfc_division_restrict_newstepprevioussum_body_steps_partial + S (fs_r_pfc_division_restrict_newstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_restrict_newstepprevioussum_body_steps)) * fs_v_pfc_division_restrict_newstepprevioussum)) /\ exists fs_q_pfc_division_restrict_newstepprevioussum_body_steps_partial. fs_u_pfc_division_restrict_newstepprevioussum = fs_q_pfc_division_restrict_newstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_restrict_newstepprevioussum_body_steps)) * fs_v_pfc_division_restrict_newstepprevioussum) + (fs_r_pfc_division_restrict_newstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_restrict_newstepprevioussum_body_steps_successor. fs_h_pfc_division_restrict_newstepprevioussum_body_steps_successor + S (fs_s_pfc_division_restrict_newstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_restrict_newstepprevioussum_body_steps)) * fs_v_pfc_division_restrict_newstepprevioussum)) /\ exists fs_q_pfc_division_restrict_newstepprevioussum_body_steps_successor. fs_u_pfc_division_restrict_newstepprevioussum = fs_q_pfc_division_restrict_newstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_restrict_newstepprevioussum_body_steps)) * fs_v_pfc_division_restrict_newstepprevioussum) + (fs_s_pfc_division_restrict_newstepprevioussum_body_steps))) /\ fs_s_pfc_division_restrict_newstepprevioussum_body_steps = fs_r_pfc_division_restrict_newstepprevioussum_body_steps + fs_a_pfc_division_restrict_newstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_restrict_newsteppreviousresiduebound. pfa_gap_division_restrict_newsteppreviousresiduebound + S (pfd_previous_division_restrict_newstep) = (p)) /\ ((exists pfa_offset_left_division_restrict_newsteppreviousresiduecongruence pfa_offset_right_division_restrict_newsteppreviousresiduecongruence. (pfc_natural_sum_division_restrict_newstepprevious) + (p) * pfa_offset_left_division_restrict_newsteppreviousresiduecongruence = (pfd_previous_division_restrict_newstep) + (p) * pfa_offset_right_division_restrict_newsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_restrict_newstepsubtractleft. pfa_gap_division_restrict_newstepsubtractleft + S (pfd_previous_division_restrict_newstep) = (p)) /\ (((exists pfa_gap_division_restrict_newstepsubtractright. pfa_gap_division_restrict_newstepsubtractright + S (pfd_difference_division_restrict_newstep) = (p)) /\ ((((exists pfa_gap_division_restrict_newstepsubtractresultbound. pfa_gap_division_restrict_newstepsubtractresultbound + S (pfd_input_division_restrict_newstep) = (p)) /\ ((exists pfa_offset_left_division_restrict_newstepsubtractresultcongruence pfa_offset_right_division_restrict_newstepsubtractresultcongruence. ((pfd_previous_division_restrict_newstep) + (pfd_difference_division_restrict_newstep)) + (p) * pfa_offset_left_division_restrict_newstepsubtractresultcongruence = (pfd_input_division_restrict_newstep) + (p) * pfa_offset_right_division_restrict_newstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_restrict_newstepmultiplyleft. pfa_gap_division_restrict_newstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_restrict_newstepmultiplyright. pfa_gap_division_restrict_newstepmultiplyright + S (pfd_difference_division_restrict_newstep) = (p)) /\ ((((exists pfa_gap_division_restrict_newstepmultiplyresultbound. pfa_gap_division_restrict_newstepmultiplyresultbound + S (pfd_value_division_restrict_new) = (p)) /\ ((exists pfa_offset_left_division_restrict_newstepmultiplyresultcongruence pfa_offset_right_division_restrict_newstepmultiplyresultcongruence. ((k) * (pfd_difference_division_restrict_newstep)) + (p) * pfa_offset_left_division_restrict_newstepmultiplyresultcongruence = (pfd_value_division_restrict_new) + (p) * pfa_offset_right_division_restrict_newstepmultiplyresultcongruence)))))))))))))))))))