prime_field_polynomial_quotient_prefix_functional

forall p k ab ac bb bc M qb qc QB QC N. (forall pfd_index_prefix_unique_first. (exists pfa_gap_prefix_unique_firstbound. pfa_gap_prefix_unique_firstbound + S (pfd_index_prefix_unique_first) = (N)) -> exists pfd_value_prefix_unique_first. ((((exists ff_h_pfp_prefix_unique_firstentry. ff_h_pfp_prefix_unique_firstentry + S (pfd_value_prefix_unique_first) = S ((S (pfd_index_prefix_unique_first)) * qc)) /\ exists ff_q_pfp_prefix_unique_firstentry. qb = ff_q_pfp_prefix_unique_firstentry * S ((S (pfd_index_prefix_unique_first)) * qc) + (pfd_value_prefix_unique_first))) /\ ((exists pfd_input_prefix_unique_firststep pfd_previous_prefix_unique_firststep pfd_difference_prefix_unique_firststep. ((((exists ff_h_pfp_prefix_unique_firststepinput. ff_h_pfp_prefix_unique_firststepinput + S (pfd_input_prefix_unique_firststep) = S ((S (pfd_index_prefix_unique_first)) * ac)) /\ exists ff_q_pfp_prefix_unique_firststepinput. ab = ff_q_pfp_prefix_unique_firststepinput * S ((S (pfd_index_prefix_unique_first)) * ac) + (pfd_input_prefix_unique_firststep))) /\ (((exists pfc_terms_code_prefix_unique_firststepprevious pfc_terms_scale_prefix_unique_firststepprevious pfc_natural_sum_prefix_unique_firststepprevious. ((forall pfc_index_prefix_unique_firststeppreviousdiagonal. (exists pfa_gap_prefix_unique_firststeppreviousdiagonalbound. pfa_gap_prefix_unique_firststeppreviousdiagonalbound + S (pfc_index_prefix_unique_firststeppreviousdiagonal) = (S (pfd_index_prefix_unique_first))) -> exists pfc_value_prefix_unique_firststeppreviousdiagonal. ((((exists ff_h_pfp_prefix_unique_firststeppreviousdiagonalentry. ff_h_pfp_prefix_unique_firststeppreviousdiagonalentry + S (pfc_value_prefix_unique_firststeppreviousdiagonal) = S ((S (pfc_index_prefix_unique_firststeppreviousdiagonal)) * pfc_terms_scale_prefix_unique_firststepprevious)) /\ exists ff_q_pfp_prefix_unique_firststeppreviousdiagonalentry. pfc_terms_code_prefix_unique_firststepprevious = ff_q_pfp_prefix_unique_firststeppreviousdiagonalentry * S ((S (pfc_index_prefix_unique_firststeppreviousdiagonal)) * pfc_terms_scale_prefix_unique_firststepprevious) + (pfc_value_prefix_unique_firststeppreviousdiagonal))) /\ ((exists pfc_complement_prefix_unique_firststeppreviousdiagonalterm pfc_left_prefix_unique_firststeppreviousdiagonalterm pfc_right_prefix_unique_firststeppreviousdiagonalterm. (((pfc_index_prefix_unique_firststeppreviousdiagonal)+pfc_complement_prefix_unique_firststeppreviousdiagonalterm=(pfd_index_prefix_unique_first)) /\ ((((((exists pfa_gap_prefix_unique_firststeppreviousdiagonaltermleftinside. pfa_gap_prefix_unique_firststeppreviousdiagonaltermleftinside + S (pfc_index_prefix_unique_firststeppreviousdiagonal) = (pfd_index_prefix_unique_first)) /\ ((((exists ff_h_pfp_prefix_unique_firststeppreviousdiagonaltermleftentry. ff_h_pfp_prefix_unique_firststeppreviousdiagonaltermleftentry + S (pfc_left_prefix_unique_firststeppreviousdiagonalterm) = S ((S (pfc_index_prefix_unique_firststeppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_prefix_unique_firststeppreviousdiagonaltermleftentry. qb = ff_q_pfp_prefix_unique_firststeppreviousdiagonaltermleftentry * S ((S (pfc_index_prefix_unique_firststeppreviousdiagonal)) * qc) + (pfc_left_prefix_unique_firststeppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_firststeppreviousdiagonaltermleftoutside. pfc_gap_prefix_unique_firststeppreviousdiagonaltermleftoutside+(pfd_index_prefix_unique_first)=(pfc_index_prefix_unique_firststeppreviousdiagonal)) /\ (((pfc_left_prefix_unique_firststeppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_prefix_unique_firststeppreviousdiagonaltermrightinside. pfa_gap_prefix_unique_firststeppreviousdiagonaltermrightinside + S (pfc_complement_prefix_unique_firststeppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_prefix_unique_firststeppreviousdiagonaltermrightentry. ff_h_pfp_prefix_unique_firststeppreviousdiagonaltermrightentry + S (pfc_right_prefix_unique_firststeppreviousdiagonalterm) = S ((S (pfc_complement_prefix_unique_firststeppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_prefix_unique_firststeppreviousdiagonaltermrightentry. bb = ff_q_pfp_prefix_unique_firststeppreviousdiagonaltermrightentry * S ((S (pfc_complement_prefix_unique_firststeppreviousdiagonalterm)) * bc) + (pfc_right_prefix_unique_firststeppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_firststeppreviousdiagonaltermrightoutside. pfc_gap_prefix_unique_firststeppreviousdiagonaltermrightoutside+(M)=(pfc_complement_prefix_unique_firststeppreviousdiagonalterm)) /\ (((pfc_right_prefix_unique_firststeppreviousdiagonalterm)=0))))) /\ (((pfc_value_prefix_unique_firststeppreviousdiagonal)=pfc_left_prefix_unique_firststeppreviousdiagonalterm*pfc_right_prefix_unique_firststeppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_prefix_unique_firststepprevioussum fs_v_pfc_prefix_unique_firststepprevioussum. ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_start. fs_h_pfc_prefix_unique_firststepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_prefix_unique_firststepprevioussum)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_start. fs_u_pfc_prefix_unique_firststepprevioussum = fs_q_pfc_prefix_unique_firststepprevioussum_body_start * S ((S (0)) * fs_v_pfc_prefix_unique_firststepprevioussum) + (0))) /\ ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_terminal. fs_h_pfc_prefix_unique_firststepprevioussum_body_terminal + S (pfc_natural_sum_prefix_unique_firststepprevious) = S ((S (S (pfd_index_prefix_unique_first))) * fs_v_pfc_prefix_unique_firststepprevioussum)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_terminal. fs_u_pfc_prefix_unique_firststepprevioussum = fs_q_pfc_prefix_unique_firststepprevioussum_body_terminal * S ((S (S (pfd_index_prefix_unique_first))) * fs_v_pfc_prefix_unique_firststepprevioussum) + (pfc_natural_sum_prefix_unique_firststepprevious))) /\ forall fs_i_pfc_prefix_unique_firststepprevioussum_body_steps. (exists fs_lt_pfc_prefix_unique_firststepprevioussum_body_steps_bound. fs_lt_pfc_prefix_unique_firststepprevioussum_body_steps_bound + S fs_i_pfc_prefix_unique_firststepprevioussum_body_steps = S (pfd_index_prefix_unique_first)) -> exists fs_a_pfc_prefix_unique_firststepprevioussum_body_steps fs_r_pfc_prefix_unique_firststepprevioussum_body_steps fs_s_pfc_prefix_unique_firststepprevioussum_body_steps. ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_summand. fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_summand + S (fs_a_pfc_prefix_unique_firststepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_firststepprevious)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_summand. pfc_terms_code_prefix_unique_firststepprevious = fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_summand * S ((S (fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_firststepprevious) + (fs_a_pfc_prefix_unique_firststepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_partial. fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_partial + S (fs_r_pfc_prefix_unique_firststepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_firststepprevioussum)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_partial. fs_u_pfc_prefix_unique_firststepprevioussum = fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_partial * S ((S (fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_firststepprevioussum) + (fs_r_pfc_prefix_unique_firststepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_successor. fs_h_pfc_prefix_unique_firststepprevioussum_body_steps_successor + S (fs_s_pfc_prefix_unique_firststepprevioussum_body_steps) = S ((S (S fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_firststepprevioussum)) /\ exists fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_successor. fs_u_pfc_prefix_unique_firststepprevioussum = fs_q_pfc_prefix_unique_firststepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_prefix_unique_firststepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_firststepprevioussum) + (fs_s_pfc_prefix_unique_firststepprevioussum_body_steps))) /\ fs_s_pfc_prefix_unique_firststepprevioussum_body_steps = fs_r_pfc_prefix_unique_firststepprevioussum_body_steps + fs_a_pfc_prefix_unique_firststepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_prefix_unique_firststeppreviousresiduebound. pfa_gap_prefix_unique_firststeppreviousresiduebound + S (pfd_previous_prefix_unique_firststep) = (p)) /\ ((exists pfa_offset_left_prefix_unique_firststeppreviousresiduecongruence pfa_offset_right_prefix_unique_firststeppreviousresiduecongruence. (pfc_natural_sum_prefix_unique_firststepprevious) + (p) * pfa_offset_left_prefix_unique_firststeppreviousresiduecongruence = (pfd_previous_prefix_unique_firststep) + (p) * pfa_offset_right_prefix_unique_firststeppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_prefix_unique_firststepsubtractleft. pfa_gap_prefix_unique_firststepsubtractleft + S (pfd_previous_prefix_unique_firststep) = (p)) /\ (((exists pfa_gap_prefix_unique_firststepsubtractright. pfa_gap_prefix_unique_firststepsubtractright + S (pfd_difference_prefix_unique_firststep) = (p)) /\ ((((exists pfa_gap_prefix_unique_firststepsubtractresultbound. pfa_gap_prefix_unique_firststepsubtractresultbound + S (pfd_input_prefix_unique_firststep) = (p)) /\ ((exists pfa_offset_left_prefix_unique_firststepsubtractresultcongruence pfa_offset_right_prefix_unique_firststepsubtractresultcongruence. ((pfd_previous_prefix_unique_firststep) + (pfd_difference_prefix_unique_firststep)) + (p) * pfa_offset_left_prefix_unique_firststepsubtractresultcongruence = (pfd_input_prefix_unique_firststep) + (p) * pfa_offset_right_prefix_unique_firststepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_prefix_unique_firststepmultiplyleft. pfa_gap_prefix_unique_firststepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_prefix_unique_firststepmultiplyright. pfa_gap_prefix_unique_firststepmultiplyright + S (pfd_difference_prefix_unique_firststep) = (p)) /\ ((((exists pfa_gap_prefix_unique_firststepmultiplyresultbound. pfa_gap_prefix_unique_firststepmultiplyresultbound + S (pfd_value_prefix_unique_first) = (p)) /\ ((exists pfa_offset_left_prefix_unique_firststepmultiplyresultcongruence pfa_offset_right_prefix_unique_firststepmultiplyresultcongruence. ((k) * (pfd_difference_prefix_unique_firststep)) + (p) * pfa_offset_left_prefix_unique_firststepmultiplyresultcongruence = (pfd_value_prefix_unique_first) + (p) * pfa_offset_right_prefix_unique_firststepmultiplyresultcongruence))))))))))))))))))) -> (forall pfd_index_prefix_unique_second. (exists pfa_gap_prefix_unique_secondbound. pfa_gap_prefix_unique_secondbound + S (pfd_index_prefix_unique_second) = (N)) -> exists pfd_value_prefix_unique_second. ((((exists ff_h_pfp_prefix_unique_secondentry. ff_h_pfp_prefix_unique_secondentry + S (pfd_value_prefix_unique_second) = S ((S (pfd_index_prefix_unique_second)) * QC)) /\ exists ff_q_pfp_prefix_unique_secondentry. QB = ff_q_pfp_prefix_unique_secondentry * S ((S (pfd_index_prefix_unique_second)) * QC) + (pfd_value_prefix_unique_second))) /\ ((exists pfd_input_prefix_unique_secondstep pfd_previous_prefix_unique_secondstep pfd_difference_prefix_unique_secondstep. ((((exists ff_h_pfp_prefix_unique_secondstepinput. ff_h_pfp_prefix_unique_secondstepinput + S (pfd_input_prefix_unique_secondstep) = S ((S (pfd_index_prefix_unique_second)) * ac)) /\ exists ff_q_pfp_prefix_unique_secondstepinput. ab = ff_q_pfp_prefix_unique_secondstepinput * S ((S (pfd_index_prefix_unique_second)) * ac) + (pfd_input_prefix_unique_secondstep))) /\ (((exists pfc_terms_code_prefix_unique_secondstepprevious pfc_terms_scale_prefix_unique_secondstepprevious pfc_natural_sum_prefix_unique_secondstepprevious. ((forall pfc_index_prefix_unique_secondsteppreviousdiagonal. (exists pfa_gap_prefix_unique_secondsteppreviousdiagonalbound. pfa_gap_prefix_unique_secondsteppreviousdiagonalbound + S (pfc_index_prefix_unique_secondsteppreviousdiagonal) = (S (pfd_index_prefix_unique_second))) -> exists pfc_value_prefix_unique_secondsteppreviousdiagonal. ((((exists ff_h_pfp_prefix_unique_secondsteppreviousdiagonalentry. ff_h_pfp_prefix_unique_secondsteppreviousdiagonalentry + S (pfc_value_prefix_unique_secondsteppreviousdiagonal) = S ((S (pfc_index_prefix_unique_secondsteppreviousdiagonal)) * pfc_terms_scale_prefix_unique_secondstepprevious)) /\ exists ff_q_pfp_prefix_unique_secondsteppreviousdiagonalentry. pfc_terms_code_prefix_unique_secondstepprevious = ff_q_pfp_prefix_unique_secondsteppreviousdiagonalentry * S ((S (pfc_index_prefix_unique_secondsteppreviousdiagonal)) * pfc_terms_scale_prefix_unique_secondstepprevious) + (pfc_value_prefix_unique_secondsteppreviousdiagonal))) /\ ((exists pfc_complement_prefix_unique_secondsteppreviousdiagonalterm pfc_left_prefix_unique_secondsteppreviousdiagonalterm pfc_right_prefix_unique_secondsteppreviousdiagonalterm. (((pfc_index_prefix_unique_secondsteppreviousdiagonal)+pfc_complement_prefix_unique_secondsteppreviousdiagonalterm=(pfd_index_prefix_unique_second)) /\ ((((((exists pfa_gap_prefix_unique_secondsteppreviousdiagonaltermleftinside. pfa_gap_prefix_unique_secondsteppreviousdiagonaltermleftinside + S (pfc_index_prefix_unique_secondsteppreviousdiagonal) = (pfd_index_prefix_unique_second)) /\ ((((exists ff_h_pfp_prefix_unique_secondsteppreviousdiagonaltermleftentry. ff_h_pfp_prefix_unique_secondsteppreviousdiagonaltermleftentry + S (pfc_left_prefix_unique_secondsteppreviousdiagonalterm) = S ((S (pfc_index_prefix_unique_secondsteppreviousdiagonal)) * QC)) /\ exists ff_q_pfp_prefix_unique_secondsteppreviousdiagonaltermleftentry. QB = ff_q_pfp_prefix_unique_secondsteppreviousdiagonaltermleftentry * S ((S (pfc_index_prefix_unique_secondsteppreviousdiagonal)) * QC) + (pfc_left_prefix_unique_secondsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_secondsteppreviousdiagonaltermleftoutside. pfc_gap_prefix_unique_secondsteppreviousdiagonaltermleftoutside+(pfd_index_prefix_unique_second)=(pfc_index_prefix_unique_secondsteppreviousdiagonal)) /\ (((pfc_left_prefix_unique_secondsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_prefix_unique_secondsteppreviousdiagonaltermrightinside. pfa_gap_prefix_unique_secondsteppreviousdiagonaltermrightinside + S (pfc_complement_prefix_unique_secondsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_prefix_unique_secondsteppreviousdiagonaltermrightentry. ff_h_pfp_prefix_unique_secondsteppreviousdiagonaltermrightentry + S (pfc_right_prefix_unique_secondsteppreviousdiagonalterm) = S ((S (pfc_complement_prefix_unique_secondsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_prefix_unique_secondsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_prefix_unique_secondsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_prefix_unique_secondsteppreviousdiagonalterm)) * bc) + (pfc_right_prefix_unique_secondsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_prefix_unique_secondsteppreviousdiagonaltermrightoutside. pfc_gap_prefix_unique_secondsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_prefix_unique_secondsteppreviousdiagonalterm)) /\ (((pfc_right_prefix_unique_secondsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_prefix_unique_secondsteppreviousdiagonal)=pfc_left_prefix_unique_secondsteppreviousdiagonalterm*pfc_right_prefix_unique_secondsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_prefix_unique_secondstepprevioussum fs_v_pfc_prefix_unique_secondstepprevioussum. ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_start. fs_h_pfc_prefix_unique_secondstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_prefix_unique_secondstepprevioussum)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_start. fs_u_pfc_prefix_unique_secondstepprevioussum = fs_q_pfc_prefix_unique_secondstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_prefix_unique_secondstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_terminal. fs_h_pfc_prefix_unique_secondstepprevioussum_body_terminal + S (pfc_natural_sum_prefix_unique_secondstepprevious) = S ((S (S (pfd_index_prefix_unique_second))) * fs_v_pfc_prefix_unique_secondstepprevioussum)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_terminal. fs_u_pfc_prefix_unique_secondstepprevioussum = fs_q_pfc_prefix_unique_secondstepprevioussum_body_terminal * S ((S (S (pfd_index_prefix_unique_second))) * fs_v_pfc_prefix_unique_secondstepprevioussum) + (pfc_natural_sum_prefix_unique_secondstepprevious))) /\ forall fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps. (exists fs_lt_pfc_prefix_unique_secondstepprevioussum_body_steps_bound. fs_lt_pfc_prefix_unique_secondstepprevioussum_body_steps_bound + S fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps = S (pfd_index_prefix_unique_second)) -> exists fs_a_pfc_prefix_unique_secondstepprevioussum_body_steps fs_r_pfc_prefix_unique_secondstepprevioussum_body_steps fs_s_pfc_prefix_unique_secondstepprevioussum_body_steps. ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_summand. fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_summand + S (fs_a_pfc_prefix_unique_secondstepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_secondstepprevious)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_summand. pfc_terms_code_prefix_unique_secondstepprevious = fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * pfc_terms_scale_prefix_unique_secondstepprevious) + (fs_a_pfc_prefix_unique_secondstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_partial. fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_partial + S (fs_r_pfc_prefix_unique_secondstepprevioussum_body_steps) = S ((S (fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_secondstepprevioussum)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_partial. fs_u_pfc_prefix_unique_secondstepprevioussum = fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_secondstepprevioussum) + (fs_r_pfc_prefix_unique_secondstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_successor. fs_h_pfc_prefix_unique_secondstepprevioussum_body_steps_successor + S (fs_s_pfc_prefix_unique_secondstepprevioussum_body_steps) = S ((S (S fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_secondstepprevioussum)) /\ exists fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_successor. fs_u_pfc_prefix_unique_secondstepprevioussum = fs_q_pfc_prefix_unique_secondstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_prefix_unique_secondstepprevioussum_body_steps)) * fs_v_pfc_prefix_unique_secondstepprevioussum) + (fs_s_pfc_prefix_unique_secondstepprevioussum_body_steps))) /\ fs_s_pfc_prefix_unique_secondstepprevioussum_body_steps = fs_r_pfc_prefix_unique_secondstepprevioussum_body_steps + fs_a_pfc_prefix_unique_secondstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_prefix_unique_secondsteppreviousresiduebound. pfa_gap_prefix_unique_secondsteppreviousresiduebound + S (pfd_previous_prefix_unique_secondstep) = (p)) /\ ((exists pfa_offset_left_prefix_unique_secondsteppreviousresiduecongruence pfa_offset_right_prefix_unique_secondsteppreviousresiduecongruence. (pfc_natural_sum_prefix_unique_secondstepprevious) + (p) * pfa_offset_left_prefix_unique_secondsteppreviousresiduecongruence = (pfd_previous_prefix_unique_secondstep) + (p) * pfa_offset_right_prefix_unique_secondsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_prefix_unique_secondstepsubtractleft. pfa_gap_prefix_unique_secondstepsubtractleft + S (pfd_previous_prefix_unique_secondstep) = (p)) /\ (((exists pfa_gap_prefix_unique_secondstepsubtractright. pfa_gap_prefix_unique_secondstepsubtractright + S (pfd_difference_prefix_unique_secondstep) = (p)) /\ ((((exists pfa_gap_prefix_unique_secondstepsubtractresultbound. pfa_gap_prefix_unique_secondstepsubtractresultbound + S (pfd_input_prefix_unique_secondstep) = (p)) /\ ((exists pfa_offset_left_prefix_unique_secondstepsubtractresultcongruence pfa_offset_right_prefix_unique_secondstepsubtractresultcongruence. ((pfd_previous_prefix_unique_secondstep) + (pfd_difference_prefix_unique_secondstep)) + (p) * pfa_offset_left_prefix_unique_secondstepsubtractresultcongruence = (pfd_input_prefix_unique_secondstep) + (p) * pfa_offset_right_prefix_unique_secondstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_prefix_unique_secondstepmultiplyleft. pfa_gap_prefix_unique_secondstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_prefix_unique_secondstepmultiplyright. pfa_gap_prefix_unique_secondstepmultiplyright + S (pfd_difference_prefix_unique_secondstep) = (p)) /\ ((((exists pfa_gap_prefix_unique_secondstepmultiplyresultbound. pfa_gap_prefix_unique_secondstepmultiplyresultbound + S (pfd_value_prefix_unique_second) = (p)) /\ ((exists pfa_offset_left_prefix_unique_secondstepmultiplyresultcongruence pfa_offset_right_prefix_unique_secondstepmultiplyresultcongruence. ((k) * (pfd_difference_prefix_unique_secondstep)) + (p) * pfa_offset_left_prefix_unique_secondstepmultiplyresultcongruence = (pfd_value_prefix_unique_second) + (p) * pfa_offset_right_prefix_unique_secondstepmultiplyresultcongruence))))))))))))))))))) -> (forall mdr_i_pfp_prefix_unique_result mdr_a_pfp_prefix_unique_result. (exists mdr_gap_pfp_prefix_unique_resultb. mdr_gap_pfp_prefix_unique_resultb + S (mdr_i_pfp_prefix_unique_result) = (N)) -> (((exists ff_h_mdr_pfp_prefix_unique_resulto. ff_h_mdr_pfp_prefix_unique_resulto + S (mdr_a_pfp_prefix_unique_result) = S ((S (mdr_i_pfp_prefix_unique_result)) * qc)) /\ exists ff_q_mdr_pfp_prefix_unique_resulto. qb = ff_q_mdr_pfp_prefix_unique_resulto * S ((S (mdr_i_pfp_prefix_unique_result)) * qc) + (mdr_a_pfp_prefix_unique_result))) -> (((exists ff_h_mdr_pfp_prefix_unique_resultn. ff_h_mdr_pfp_prefix_unique_resultn + S (mdr_a_pfp_prefix_unique_result) = S ((S (mdr_i_pfp_prefix_unique_result)) * QC)) /\ exists ff_q_mdr_pfp_prefix_unique_resultn. QB = ff_q_mdr_pfp_prefix_unique_resultn * S ((S (mdr_i_pfp_prefix_unique_result)) * QC) + (mdr_a_pfp_prefix_unique_result))))