prime_field_polynomial_quotient_prefix_append

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc M qb qc QB QC N q. (forall pfd_index_division_append_old. (exists pfa_gap_division_append_oldbound. pfa_gap_division_append_oldbound + S (pfd_index_division_append_old) = (N)) -> exists pfd_value_division_append_old. ((((exists ff_h_pfp_division_append_oldentry. ff_h_pfp_division_append_oldentry + S (pfd_value_division_append_old) = S ((S (pfd_index_division_append_old)) * qc)) /\ exists ff_q_pfp_division_append_oldentry. qb = ff_q_pfp_division_append_oldentry * S ((S (pfd_index_division_append_old)) * qc) + (pfd_value_division_append_old))) /\ ((exists pfd_input_division_append_oldstep pfd_previous_division_append_oldstep pfd_difference_division_append_oldstep. ((((exists ff_h_pfp_division_append_oldstepinput. ff_h_pfp_division_append_oldstepinput + S (pfd_input_division_append_oldstep) = S ((S (pfd_index_division_append_old)) * ac)) /\ exists ff_q_pfp_division_append_oldstepinput. ab = ff_q_pfp_division_append_oldstepinput * S ((S (pfd_index_division_append_old)) * ac) + (pfd_input_division_append_oldstep))) /\ (((exists pfc_terms_code_division_append_oldstepprevious pfc_terms_scale_division_append_oldstepprevious pfc_natural_sum_division_append_oldstepprevious. ((forall pfc_index_division_append_oldsteppreviousdiagonal. (exists pfa_gap_division_append_oldsteppreviousdiagonalbound. pfa_gap_division_append_oldsteppreviousdiagonalbound + S (pfc_index_division_append_oldsteppreviousdiagonal) = (S (pfd_index_division_append_old))) -> exists pfc_value_division_append_oldsteppreviousdiagonal. ((((exists ff_h_pfp_division_append_oldsteppreviousdiagonalentry. ff_h_pfp_division_append_oldsteppreviousdiagonalentry + S (pfc_value_division_append_oldsteppreviousdiagonal) = S ((S (pfc_index_division_append_oldsteppreviousdiagonal)) * pfc_terms_scale_division_append_oldstepprevious)) /\ exists ff_q_pfp_division_append_oldsteppreviousdiagonalentry. pfc_terms_code_division_append_oldstepprevious = ff_q_pfp_division_append_oldsteppreviousdiagonalentry * S ((S (pfc_index_division_append_oldsteppreviousdiagonal)) * pfc_terms_scale_division_append_oldstepprevious) + (pfc_value_division_append_oldsteppreviousdiagonal))) /\ ((exists pfc_complement_division_append_oldsteppreviousdiagonalterm pfc_left_division_append_oldsteppreviousdiagonalterm pfc_right_division_append_oldsteppreviousdiagonalterm. (((pfc_index_division_append_oldsteppreviousdiagonal)+pfc_complement_division_append_oldsteppreviousdiagonalterm=(pfd_index_division_append_old)) /\ ((((((exists pfa_gap_division_append_oldsteppreviousdiagonaltermleftinside. pfa_gap_division_append_oldsteppreviousdiagonaltermleftinside + S (pfc_index_division_append_oldsteppreviousdiagonal) = (pfd_index_division_append_old)) /\ ((((exists ff_h_pfp_division_append_oldsteppreviousdiagonaltermleftentry. ff_h_pfp_division_append_oldsteppreviousdiagonaltermleftentry + S (pfc_left_division_append_oldsteppreviousdiagonalterm) = S ((S (pfc_index_division_append_oldsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_append_oldsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_append_oldsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_append_oldsteppreviousdiagonal)) * qc) + (pfc_left_division_append_oldsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_oldsteppreviousdiagonaltermleftoutside. pfc_gap_division_append_oldsteppreviousdiagonaltermleftoutside+(pfd_index_division_append_old)=(pfc_index_division_append_oldsteppreviousdiagonal)) /\ (((pfc_left_division_append_oldsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_append_oldsteppreviousdiagonaltermrightinside. pfa_gap_division_append_oldsteppreviousdiagonaltermrightinside + S (pfc_complement_division_append_oldsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_append_oldsteppreviousdiagonaltermrightentry. ff_h_pfp_division_append_oldsteppreviousdiagonaltermrightentry + S (pfc_right_division_append_oldsteppreviousdiagonalterm) = S ((S (pfc_complement_division_append_oldsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_append_oldsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_append_oldsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_append_oldsteppreviousdiagonalterm)) * bc) + (pfc_right_division_append_oldsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_oldsteppreviousdiagonaltermrightoutside. pfc_gap_division_append_oldsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_append_oldsteppreviousdiagonalterm)) /\ (((pfc_right_division_append_oldsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_append_oldsteppreviousdiagonal)=pfc_left_division_append_oldsteppreviousdiagonalterm*pfc_right_division_append_oldsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_append_oldstepprevioussum fs_v_pfc_division_append_oldstepprevioussum. ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_start. fs_h_pfc_division_append_oldstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_append_oldstepprevioussum)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_start. fs_u_pfc_division_append_oldstepprevioussum = fs_q_pfc_division_append_oldstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_append_oldstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_terminal. fs_h_pfc_division_append_oldstepprevioussum_body_terminal + S (pfc_natural_sum_division_append_oldstepprevious) = S ((S (S (pfd_index_division_append_old))) * fs_v_pfc_division_append_oldstepprevioussum)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_terminal. fs_u_pfc_division_append_oldstepprevioussum = fs_q_pfc_division_append_oldstepprevioussum_body_terminal * S ((S (S (pfd_index_division_append_old))) * fs_v_pfc_division_append_oldstepprevioussum) + (pfc_natural_sum_division_append_oldstepprevious))) /\ forall fs_i_pfc_division_append_oldstepprevioussum_body_steps. (exists fs_lt_pfc_division_append_oldstepprevioussum_body_steps_bound. fs_lt_pfc_division_append_oldstepprevioussum_body_steps_bound + S fs_i_pfc_division_append_oldstepprevioussum_body_steps = S (pfd_index_division_append_old)) -> exists fs_a_pfc_division_append_oldstepprevioussum_body_steps fs_r_pfc_division_append_oldstepprevioussum_body_steps fs_s_pfc_division_append_oldstepprevioussum_body_steps. ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_steps_summand. fs_h_pfc_division_append_oldstepprevioussum_body_steps_summand + S (fs_a_pfc_division_append_oldstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * pfc_terms_scale_division_append_oldstepprevious)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_steps_summand. pfc_terms_code_division_append_oldstepprevious = fs_q_pfc_division_append_oldstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * pfc_terms_scale_division_append_oldstepprevious) + (fs_a_pfc_division_append_oldstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_steps_partial. fs_h_pfc_division_append_oldstepprevioussum_body_steps_partial + S (fs_r_pfc_division_append_oldstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * fs_v_pfc_division_append_oldstepprevioussum)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_steps_partial. fs_u_pfc_division_append_oldstepprevioussum = fs_q_pfc_division_append_oldstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * fs_v_pfc_division_append_oldstepprevioussum) + (fs_r_pfc_division_append_oldstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_steps_successor. fs_h_pfc_division_append_oldstepprevioussum_body_steps_successor + S (fs_s_pfc_division_append_oldstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * fs_v_pfc_division_append_oldstepprevioussum)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_steps_successor. fs_u_pfc_division_append_oldstepprevioussum = fs_q_pfc_division_append_oldstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * fs_v_pfc_division_append_oldstepprevioussum) + (fs_s_pfc_division_append_oldstepprevioussum_body_steps))) /\ fs_s_pfc_division_append_oldstepprevioussum_body_steps = fs_r_pfc_division_append_oldstepprevioussum_body_steps + fs_a_pfc_division_append_oldstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_append_oldsteppreviousresiduebound. pfa_gap_division_append_oldsteppreviousresiduebound + S (pfd_previous_division_append_oldstep) = (p)) /\ ((exists pfa_offset_left_division_append_oldsteppreviousresiduecongruence pfa_offset_right_division_append_oldsteppreviousresiduecongruence. (pfc_natural_sum_division_append_oldstepprevious) + (p) * pfa_offset_left_division_append_oldsteppreviousresiduecongruence = (pfd_previous_division_append_oldstep) + (p) * pfa_offset_right_division_append_oldsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_append_oldstepsubtractleft. pfa_gap_division_append_oldstepsubtractleft + S (pfd_previous_division_append_oldstep) = (p)) /\ (((exists pfa_gap_division_append_oldstepsubtractright. pfa_gap_division_append_oldstepsubtractright + S (pfd_difference_division_append_oldstep) = (p)) /\ ((((exists pfa_gap_division_append_oldstepsubtractresultbound. pfa_gap_division_append_oldstepsubtractresultbound + S (pfd_input_division_append_oldstep) = (p)) /\ ((exists pfa_offset_left_division_append_oldstepsubtractresultcongruence pfa_offset_right_division_append_oldstepsubtractresultcongruence. ((pfd_previous_division_append_oldstep) + (pfd_difference_division_append_oldstep)) + (p) * pfa_offset_left_division_append_oldstepsubtractresultcongruence = (pfd_input_division_append_oldstep) + (p) * pfa_offset_right_division_append_oldstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_append_oldstepmultiplyleft. pfa_gap_division_append_oldstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_append_oldstepmultiplyright. pfa_gap_division_append_oldstepmultiplyright + S (pfd_difference_division_append_oldstep) = (p)) /\ ((((exists pfa_gap_division_append_oldstepmultiplyresultbound. pfa_gap_division_append_oldstepmultiplyresultbound + S (pfd_value_division_append_old) = (p)) /\ ((exists pfa_offset_left_division_append_oldstepmultiplyresultcongruence pfa_offset_right_division_append_oldstepmultiplyresultcongruence. ((k) * (pfd_difference_division_append_oldstep)) + (p) * pfa_offset_left_division_append_oldstepmultiplyresultcongruence = (pfd_value_division_append_old) + (p) * pfa_offset_right_division_append_oldstepmultiplyresultcongruence))))))))))))))))))) -> (forall mdr_i_pfp_division_append_equal mdr_a_pfp_division_append_equal. (exists mdr_gap_pfp_division_append_equalb. mdr_gap_pfp_division_append_equalb + S (mdr_i_pfp_division_append_equal) = (N)) -> (((exists ff_h_mdr_pfp_division_append_equalo. ff_h_mdr_pfp_division_append_equalo + S (mdr_a_pfp_division_append_equal) = S ((S (mdr_i_pfp_division_append_equal)) * qc)) /\ exists ff_q_mdr_pfp_division_append_equalo. qb = ff_q_mdr_pfp_division_append_equalo * S ((S (mdr_i_pfp_division_append_equal)) * qc) + (mdr_a_pfp_division_append_equal))) -> (((exists ff_h_mdr_pfp_division_append_equaln. ff_h_mdr_pfp_division_append_equaln + S (mdr_a_pfp_division_append_equal) = S ((S (mdr_i_pfp_division_append_equal)) * QC)) /\ exists ff_q_mdr_pfp_division_append_equaln. QB = ff_q_mdr_pfp_division_append_equaln * S ((S (mdr_i_pfp_division_append_equal)) * QC) + (mdr_a_pfp_division_append_equal)))) -> (((exists ff_h_pfp_division_append_given_entry. ff_h_pfp_division_append_given_entry + S (q) = S ((S (N)) * QC)) /\ exists ff_q_pfp_division_append_given_entry. QB = ff_q_pfp_division_append_given_entry * S ((S (N)) * QC) + (q))) -> (exists pfd_input_division_append_given_step pfd_previous_division_append_given_step pfd_difference_division_append_given_step. ((((exists ff_h_pfp_division_append_given_stepinput. ff_h_pfp_division_append_given_stepinput + S (pfd_input_division_append_given_step) = S ((S (N)) * ac)) /\ exists ff_q_pfp_division_append_given_stepinput. ab = ff_q_pfp_division_append_given_stepinput * S ((S (N)) * ac) + (pfd_input_division_append_given_step))) /\ (((exists pfc_terms_code_division_append_given_stepprevious pfc_terms_scale_division_append_given_stepprevious pfc_natural_sum_division_append_given_stepprevious. ((forall pfc_index_division_append_given_steppreviousdiagonal. (exists pfa_gap_division_append_given_steppreviousdiagonalbound. pfa_gap_division_append_given_steppreviousdiagonalbound + S (pfc_index_division_append_given_steppreviousdiagonal) = (S (N))) -> exists pfc_value_division_append_given_steppreviousdiagonal. ((((exists ff_h_pfp_division_append_given_steppreviousdiagonalentry. ff_h_pfp_division_append_given_steppreviousdiagonalentry + S (pfc_value_division_append_given_steppreviousdiagonal) = S ((S (pfc_index_division_append_given_steppreviousdiagonal)) * pfc_terms_scale_division_append_given_stepprevious)) /\ exists ff_q_pfp_division_append_given_steppreviousdiagonalentry. pfc_terms_code_division_append_given_stepprevious = ff_q_pfp_division_append_given_steppreviousdiagonalentry * S ((S (pfc_index_division_append_given_steppreviousdiagonal)) * pfc_terms_scale_division_append_given_stepprevious) + (pfc_value_division_append_given_steppreviousdiagonal))) /\ ((exists pfc_complement_division_append_given_steppreviousdiagonalterm pfc_left_division_append_given_steppreviousdiagonalterm pfc_right_division_append_given_steppreviousdiagonalterm. (((pfc_index_division_append_given_steppreviousdiagonal)+pfc_complement_division_append_given_steppreviousdiagonalterm=(N)) /\ ((((((exists pfa_gap_division_append_given_steppreviousdiagonaltermleftinside. pfa_gap_division_append_given_steppreviousdiagonaltermleftinside + S (pfc_index_division_append_given_steppreviousdiagonal) = (N)) /\ ((((exists ff_h_pfp_division_append_given_steppreviousdiagonaltermleftentry. ff_h_pfp_division_append_given_steppreviousdiagonaltermleftentry + S (pfc_left_division_append_given_steppreviousdiagonalterm) = S ((S (pfc_index_division_append_given_steppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_append_given_steppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_append_given_steppreviousdiagonaltermleftentry * S ((S (pfc_index_division_append_given_steppreviousdiagonal)) * qc) + (pfc_left_division_append_given_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_given_steppreviousdiagonaltermleftoutside. pfc_gap_division_append_given_steppreviousdiagonaltermleftoutside+(N)=(pfc_index_division_append_given_steppreviousdiagonal)) /\ (((pfc_left_division_append_given_steppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_append_given_steppreviousdiagonaltermrightinside. pfa_gap_division_append_given_steppreviousdiagonaltermrightinside + S (pfc_complement_division_append_given_steppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_append_given_steppreviousdiagonaltermrightentry. ff_h_pfp_division_append_given_steppreviousdiagonaltermrightentry + S (pfc_right_division_append_given_steppreviousdiagonalterm) = S ((S (pfc_complement_division_append_given_steppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_append_given_steppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_append_given_steppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_append_given_steppreviousdiagonalterm)) * bc) + (pfc_right_division_append_given_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_given_steppreviousdiagonaltermrightoutside. pfc_gap_division_append_given_steppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_append_given_steppreviousdiagonalterm)) /\ (((pfc_right_division_append_given_steppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_append_given_steppreviousdiagonal)=pfc_left_division_append_given_steppreviousdiagonalterm*pfc_right_division_append_given_steppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_append_given_stepprevioussum fs_v_pfc_division_append_given_stepprevioussum. ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_start. fs_h_pfc_division_append_given_stepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_append_given_stepprevioussum)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_start. fs_u_pfc_division_append_given_stepprevioussum = fs_q_pfc_division_append_given_stepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_append_given_stepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_terminal. fs_h_pfc_division_append_given_stepprevioussum_body_terminal + S (pfc_natural_sum_division_append_given_stepprevious) = S ((S (S (N))) * fs_v_pfc_division_append_given_stepprevioussum)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_terminal. fs_u_pfc_division_append_given_stepprevioussum = fs_q_pfc_division_append_given_stepprevioussum_body_terminal * S ((S (S (N))) * fs_v_pfc_division_append_given_stepprevioussum) + (pfc_natural_sum_division_append_given_stepprevious))) /\ forall fs_i_pfc_division_append_given_stepprevioussum_body_steps. (exists fs_lt_pfc_division_append_given_stepprevioussum_body_steps_bound. fs_lt_pfc_division_append_given_stepprevioussum_body_steps_bound + S fs_i_pfc_division_append_given_stepprevioussum_body_steps = S (N)) -> exists fs_a_pfc_division_append_given_stepprevioussum_body_steps fs_r_pfc_division_append_given_stepprevioussum_body_steps fs_s_pfc_division_append_given_stepprevioussum_body_steps. ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_steps_summand. fs_h_pfc_division_append_given_stepprevioussum_body_steps_summand + S (fs_a_pfc_division_append_given_stepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * pfc_terms_scale_division_append_given_stepprevious)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_steps_summand. pfc_terms_code_division_append_given_stepprevious = fs_q_pfc_division_append_given_stepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * pfc_terms_scale_division_append_given_stepprevious) + (fs_a_pfc_division_append_given_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_steps_partial. fs_h_pfc_division_append_given_stepprevioussum_body_steps_partial + S (fs_r_pfc_division_append_given_stepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * fs_v_pfc_division_append_given_stepprevioussum)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_steps_partial. fs_u_pfc_division_append_given_stepprevioussum = fs_q_pfc_division_append_given_stepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * fs_v_pfc_division_append_given_stepprevioussum) + (fs_r_pfc_division_append_given_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_steps_successor. fs_h_pfc_division_append_given_stepprevioussum_body_steps_successor + S (fs_s_pfc_division_append_given_stepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * fs_v_pfc_division_append_given_stepprevioussum)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_steps_successor. fs_u_pfc_division_append_given_stepprevioussum = fs_q_pfc_division_append_given_stepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * fs_v_pfc_division_append_given_stepprevioussum) + (fs_s_pfc_division_append_given_stepprevioussum_body_steps))) /\ fs_s_pfc_division_append_given_stepprevioussum_body_steps = fs_r_pfc_division_append_given_stepprevioussum_body_steps + fs_a_pfc_division_append_given_stepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_append_given_steppreviousresiduebound. pfa_gap_division_append_given_steppreviousresiduebound + S (pfd_previous_division_append_given_step) = (p)) /\ ((exists pfa_offset_left_division_append_given_steppreviousresiduecongruence pfa_offset_right_division_append_given_steppreviousresiduecongruence. (pfc_natural_sum_division_append_given_stepprevious) + (p) * pfa_offset_left_division_append_given_steppreviousresiduecongruence = (pfd_previous_division_append_given_step) + (p) * pfa_offset_right_division_append_given_steppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_append_given_stepsubtractleft. pfa_gap_division_append_given_stepsubtractleft + S (pfd_previous_division_append_given_step) = (p)) /\ (((exists pfa_gap_division_append_given_stepsubtractright. pfa_gap_division_append_given_stepsubtractright + S (pfd_difference_division_append_given_step) = (p)) /\ ((((exists pfa_gap_division_append_given_stepsubtractresultbound. pfa_gap_division_append_given_stepsubtractresultbound + S (pfd_input_division_append_given_step) = (p)) /\ ((exists pfa_offset_left_division_append_given_stepsubtractresultcongruence pfa_offset_right_division_append_given_stepsubtractresultcongruence. ((pfd_previous_division_append_given_step) + (pfd_difference_division_append_given_step)) + (p) * pfa_offset_left_division_append_given_stepsubtractresultcongruence = (pfd_input_division_append_given_step) + (p) * pfa_offset_right_division_append_given_stepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_append_given_stepmultiplyleft. pfa_gap_division_append_given_stepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_append_given_stepmultiplyright. pfa_gap_division_append_given_stepmultiplyright + S (pfd_difference_division_append_given_step) = (p)) /\ ((((exists pfa_gap_division_append_given_stepmultiplyresultbound. pfa_gap_division_append_given_stepmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_division_append_given_stepmultiplyresultcongruence pfa_offset_right_division_append_given_stepmultiplyresultcongruence. ((k) * (pfd_difference_division_append_given_step)) + (p) * pfa_offset_left_division_append_given_stepmultiplyresultcongruence = (q) + (p) * pfa_offset_right_division_append_given_stepmultiplyresultcongruence)))))))))))))))) -> (forall pfd_index_division_append_new. (exists pfa_gap_division_append_newbound. pfa_gap_division_append_newbound + S (pfd_index_division_append_new) = (S N)) -> exists pfd_value_division_append_new. ((((exists ff_h_pfp_division_append_newentry. ff_h_pfp_division_append_newentry + S (pfd_value_division_append_new) = S ((S (pfd_index_division_append_new)) * QC)) /\ exists ff_q_pfp_division_append_newentry. QB = ff_q_pfp_division_append_newentry * S ((S (pfd_index_division_append_new)) * QC) + (pfd_value_division_append_new))) /\ ((exists pfd_input_division_append_newstep pfd_previous_division_append_newstep pfd_difference_division_append_newstep. ((((exists ff_h_pfp_division_append_newstepinput. ff_h_pfp_division_append_newstepinput + S (pfd_input_division_append_newstep) = S ((S (pfd_index_division_append_new)) * ac)) /\ exists ff_q_pfp_division_append_newstepinput. ab = ff_q_pfp_division_append_newstepinput * S ((S (pfd_index_division_append_new)) * ac) + (pfd_input_division_append_newstep))) /\ (((exists pfc_terms_code_division_append_newstepprevious pfc_terms_scale_division_append_newstepprevious pfc_natural_sum_division_append_newstepprevious. ((forall pfc_index_division_append_newsteppreviousdiagonal. (exists pfa_gap_division_append_newsteppreviousdiagonalbound. pfa_gap_division_append_newsteppreviousdiagonalbound + S (pfc_index_division_append_newsteppreviousdiagonal) = (S (pfd_index_division_append_new))) -> exists pfc_value_division_append_newsteppreviousdiagonal. ((((exists ff_h_pfp_division_append_newsteppreviousdiagonalentry. ff_h_pfp_division_append_newsteppreviousdiagonalentry + S (pfc_value_division_append_newsteppreviousdiagonal) = S ((S (pfc_index_division_append_newsteppreviousdiagonal)) * pfc_terms_scale_division_append_newstepprevious)) /\ exists ff_q_pfp_division_append_newsteppreviousdiagonalentry. pfc_terms_code_division_append_newstepprevious = ff_q_pfp_division_append_newsteppreviousdiagonalentry * S ((S (pfc_index_division_append_newsteppreviousdiagonal)) * pfc_terms_scale_division_append_newstepprevious) + (pfc_value_division_append_newsteppreviousdiagonal))) /\ ((exists pfc_complement_division_append_newsteppreviousdiagonalterm pfc_left_division_append_newsteppreviousdiagonalterm pfc_right_division_append_newsteppreviousdiagonalterm. (((pfc_index_division_append_newsteppreviousdiagonal)+pfc_complement_division_append_newsteppreviousdiagonalterm=(pfd_index_division_append_new)) /\ ((((((exists pfa_gap_division_append_newsteppreviousdiagonaltermleftinside. pfa_gap_division_append_newsteppreviousdiagonaltermleftinside + S (pfc_index_division_append_newsteppreviousdiagonal) = (pfd_index_division_append_new)) /\ ((((exists ff_h_pfp_division_append_newsteppreviousdiagonaltermleftentry. ff_h_pfp_division_append_newsteppreviousdiagonaltermleftentry + S (pfc_left_division_append_newsteppreviousdiagonalterm) = S ((S (pfc_index_division_append_newsteppreviousdiagonal)) * QC)) /\ exists ff_q_pfp_division_append_newsteppreviousdiagonaltermleftentry. QB = ff_q_pfp_division_append_newsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_append_newsteppreviousdiagonal)) * QC) + (pfc_left_division_append_newsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_newsteppreviousdiagonaltermleftoutside. pfc_gap_division_append_newsteppreviousdiagonaltermleftoutside+(pfd_index_division_append_new)=(pfc_index_division_append_newsteppreviousdiagonal)) /\ (((pfc_left_division_append_newsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_append_newsteppreviousdiagonaltermrightinside. pfa_gap_division_append_newsteppreviousdiagonaltermrightinside + S (pfc_complement_division_append_newsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_append_newsteppreviousdiagonaltermrightentry. ff_h_pfp_division_append_newsteppreviousdiagonaltermrightentry + S (pfc_right_division_append_newsteppreviousdiagonalterm) = S ((S (pfc_complement_division_append_newsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_append_newsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_append_newsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_append_newsteppreviousdiagonalterm)) * bc) + (pfc_right_division_append_newsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_newsteppreviousdiagonaltermrightoutside. pfc_gap_division_append_newsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_append_newsteppreviousdiagonalterm)) /\ (((pfc_right_division_append_newsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_append_newsteppreviousdiagonal)=pfc_left_division_append_newsteppreviousdiagonalterm*pfc_right_division_append_newsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_append_newstepprevioussum fs_v_pfc_division_append_newstepprevioussum. ((((exists fs_h_pfc_division_append_newstepprevioussum_body_start. fs_h_pfc_division_append_newstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_append_newstepprevioussum)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_start. fs_u_pfc_division_append_newstepprevioussum = fs_q_pfc_division_append_newstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_append_newstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_append_newstepprevioussum_body_terminal. fs_h_pfc_division_append_newstepprevioussum_body_terminal + S (pfc_natural_sum_division_append_newstepprevious) = S ((S (S (pfd_index_division_append_new))) * fs_v_pfc_division_append_newstepprevioussum)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_terminal. fs_u_pfc_division_append_newstepprevioussum = fs_q_pfc_division_append_newstepprevioussum_body_terminal * S ((S (S (pfd_index_division_append_new))) * fs_v_pfc_division_append_newstepprevioussum) + (pfc_natural_sum_division_append_newstepprevious))) /\ forall fs_i_pfc_division_append_newstepprevioussum_body_steps. (exists fs_lt_pfc_division_append_newstepprevioussum_body_steps_bound. fs_lt_pfc_division_append_newstepprevioussum_body_steps_bound + S fs_i_pfc_division_append_newstepprevioussum_body_steps = S (pfd_index_division_append_new)) -> exists fs_a_pfc_division_append_newstepprevioussum_body_steps fs_r_pfc_division_append_newstepprevioussum_body_steps fs_s_pfc_division_append_newstepprevioussum_body_steps. ((((exists fs_h_pfc_division_append_newstepprevioussum_body_steps_summand. fs_h_pfc_division_append_newstepprevioussum_body_steps_summand + S (fs_a_pfc_division_append_newstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_newstepprevioussum_body_steps)) * pfc_terms_scale_division_append_newstepprevious)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_steps_summand. pfc_terms_code_division_append_newstepprevious = fs_q_pfc_division_append_newstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_append_newstepprevioussum_body_steps)) * pfc_terms_scale_division_append_newstepprevious) + (fs_a_pfc_division_append_newstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_newstepprevioussum_body_steps_partial. fs_h_pfc_division_append_newstepprevioussum_body_steps_partial + S (fs_r_pfc_division_append_newstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_newstepprevioussum_body_steps)) * fs_v_pfc_division_append_newstepprevioussum)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_steps_partial. fs_u_pfc_division_append_newstepprevioussum = fs_q_pfc_division_append_newstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_append_newstepprevioussum_body_steps)) * fs_v_pfc_division_append_newstepprevioussum) + (fs_r_pfc_division_append_newstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_newstepprevioussum_body_steps_successor. fs_h_pfc_division_append_newstepprevioussum_body_steps_successor + S (fs_s_pfc_division_append_newstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_append_newstepprevioussum_body_steps)) * fs_v_pfc_division_append_newstepprevioussum)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_steps_successor. fs_u_pfc_division_append_newstepprevioussum = fs_q_pfc_division_append_newstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_append_newstepprevioussum_body_steps)) * fs_v_pfc_division_append_newstepprevioussum) + (fs_s_pfc_division_append_newstepprevioussum_body_steps))) /\ fs_s_pfc_division_append_newstepprevioussum_body_steps = fs_r_pfc_division_append_newstepprevioussum_body_steps + fs_a_pfc_division_append_newstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_append_newsteppreviousresiduebound. pfa_gap_division_append_newsteppreviousresiduebound + S (pfd_previous_division_append_newstep) = (p)) /\ ((exists pfa_offset_left_division_append_newsteppreviousresiduecongruence pfa_offset_right_division_append_newsteppreviousresiduecongruence. (pfc_natural_sum_division_append_newstepprevious) + (p) * pfa_offset_left_division_append_newsteppreviousresiduecongruence = (pfd_previous_division_append_newstep) + (p) * pfa_offset_right_division_append_newsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_append_newstepsubtractleft. pfa_gap_division_append_newstepsubtractleft + S (pfd_previous_division_append_newstep) = (p)) /\ (((exists pfa_gap_division_append_newstepsubtractright. pfa_gap_division_append_newstepsubtractright + S (pfd_difference_division_append_newstep) = (p)) /\ ((((exists pfa_gap_division_append_newstepsubtractresultbound. pfa_gap_division_append_newstepsubtractresultbound + S (pfd_input_division_append_newstep) = (p)) /\ ((exists pfa_offset_left_division_append_newstepsubtractresultcongruence pfa_offset_right_division_append_newstepsubtractresultcongruence. ((pfd_previous_division_append_newstep) + (pfd_difference_division_append_newstep)) + (p) * pfa_offset_left_division_append_newstepsubtractresultcongruence = (pfd_input_division_append_newstep) + (p) * pfa_offset_right_division_append_newstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_append_newstepmultiplyleft. pfa_gap_division_append_newstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_append_newstepmultiplyright. pfa_gap_division_append_newstepmultiplyright + S (pfd_difference_division_append_newstep) = (p)) /\ ((((exists pfa_gap_division_append_newstepmultiplyresultbound. pfa_gap_division_append_newstepmultiplyresultbound + S (pfd_value_division_append_new) = (p)) /\ ((exists pfa_offset_left_division_append_newstepmultiplyresultcongruence pfa_offset_right_division_append_newstepmultiplyresultcongruence. ((k) * (pfd_difference_division_append_newstep)) + (p) * pfa_offset_left_division_append_newstepmultiplyresultcongruence = (pfd_value_division_append_new) + (p) * pfa_offset_right_division_append_newstepmultiplyresultcongruence)))))))))))))))))))